module

public import Mathlib.Data.Prod.Lex
public import Mathlib.RingTheory.Coprime.Basic
public import Mathlib.Algebra.Star.SelfAdjoint
public import Mathlib.Topology.Algebra.Group.Basic
import all Mathlib.Data.Prod.Lex
meta import AutoGeneralization

public section

namespace AutoGeneralizationTest.Examples

/-! User-facing examples using only the public command and linter syntax. -/

class Weak (α : Type) where
  op : α → α

class Middle (α : Type) extends Weak α where
  tr : True

class Strong (α : Type) extends Middle α where
  size : Nat

theorem typeClassSource {α : Type} [Strong α] (x : α) :
    Weak.op x = Weak.op x :=
  rfl

-- Inspect every candidate. Clicking `[apply]` inserts its theorem below the command.
/--
info: Type class generalization candidates for AutoGeneralizationTest.Examples.typeClassSource (1 found):
  [apply] candidate 1/1: [Strong α] → [Weak α]
    result: theorem typeClassSource_generalized {α : Type} [Weak α] (x : α) : Weak.op x = Weak.op x
-/
#guard_msgs in
#autogeneralize typeClassSource

-- Source inserted by the candidate's code action.
theorem typeClassSource_generalized {α : Type} [Weak α] (x : α) : Weak.op x = Weak.op x :=
  rfl

theorem dependentTypeClassSource {α : Type} [Strong α] (x : α)
    (h : Weak.op x = x) : h = h :=
  rfl

/--
info: Type class generalization candidates for AutoGeneralizationTest.Examples.dependentTypeClassSource (1 found):
  [apply] candidate 1/1: [Strong α] → [Weak α]
    result: theorem dependentTypeClassSource_generalized {α : Type} [Weak α] (x : α) (h : Weak.op x = x) : h = h
-/
#guard_msgs in
#autogeneralize dependentTypeClassSource

theorem dependentTypeClassSource_generalized {α : Type} [Weak α] (x : α)
    (h : Weak.op x = x) : h = h :=
  rfl

/-- A dependency on a field of the stronger class cannot be removed yet. -/
theorem strongFieldDependency {α : Type} [s : Strong α]
    (_ : Fin (s.size + 1)) (x : α) : Weak.op x = Weak.op x :=
  rfl

/--
info: No type class generalization found for AutoGeneralizationTest.Examples.strongFieldDependency.
-/
#guard_msgs in
#autogeneralize strongFieldDependency

/--
error: -- Found 2 errors in 17 declarations (plus 23 automatically generated ones) in the current file with 1 linters

/- The `generalizeTypeClass` linter reports:
THEOREM TYPECLASS ASSUMPTIONS CAN BE GENERALIZED:
This linter can be disabled with `@[nolint generalizeTypeClass]`. -/
#check @typeClassSource /- [inst✝ : Strong α] can be generalized to [Weak α] -/
#check @dependentTypeClassSource /- [inst✝ : Strong α] can be generalized to [Weak α] -/
-/
#guard_msgs in
#lint only generalizeTypeClass

-- A later binder may depend on a field supplied by the weaker class.
class HasBound (α : Type) where
  bound : Nat

class RichBound (α : Type) extends HasBound α where
  tag : Nat

theorem dependentIndexSource {α : Type} [RichBound α]
    (i : Fin (HasBound.bound (α := α) + 1)) : i = i :=
  rfl

/--
info: Type class generalization candidates for AutoGeneralizationTest.Examples.dependentIndexSource (1 found):
  [apply] candidate 1/1: [RichBound α] → [HasBound α]
    result: theorem dependentIndexSource_generalized {α : Type} [HasBound α] (i : Fin (HasBound.bound α + 1)) : i = i
-/
#guard_msgs in
#autogeneralize dependentIndexSource

theorem dependentIndexSource_generalized {α : Type} [HasBound α]
    (i : Fin (HasBound.bound α + 1)) : i = i :=
  rfl

-- If the weaker class depends on a later argument, its binder moves after it.
class Seeded (α : Type) where
  seed : Nat

class AtPoint (α : Type) (x : α) where
  measure : Nat

instance atPointOfSeeded {α : Type} [s : Seeded α] (x : α) : AtPoint α x where
  measure := s.seed

theorem reorderedSource {α : Type} [Seeded α] (x : α) :
    AtPoint.measure (α := α) (x := x) = AtPoint.measure (α := α) (x := x) :=
  rfl

/--
info: Type class generalization candidates for AutoGeneralizationTest.Examples.reorderedSource (1 found):
  [apply] candidate 1/1: [Seeded α] → [AtPoint α x]
    result: theorem reorderedSource_generalized {α : Type} (x : α) [AtPoint α x] : AtPoint.measure x = AtPoint.measure x
-/
#guard_msgs in
#autogeneralize reorderedSource

theorem reorderedSource_generalized {α : Type} (x : α) [AtPoint α x] :
    AtPoint.measure (α := α) (x := x) = AtPoint.measure (α := α) (x := x) :=
  rfl

/-! ### Generalizing a Mathlib theorem with two capabilities -/

open Prod

/-
The command can inspect this imported theorem directly. Its current signature
is already minimal.
-/
/-- info: No type class generalization found for Prod.Lex.toLex_le_toLex. -/
#guard_msgs in
#autogeneralize Prod.Lex.toLex_le_toLex

/--
`Prod.Lex.toLex_le_toLex` needs only `LT` on the first component and `LE` on the
second. Using the same type twice splits one `Preorder` into two evidence binders.
-/
theorem lexicographicSelf {α : Type} [Preorder α] {x y : α × α} :
    toLex x ≤ toLex y ↔ x.1 < y.1 ∨ x.1 = y.1 ∧ x.2 ≤ y.2 :=
  Prod.Lex.toLex_le_toLex

/--
info: Type class generalization candidates for AutoGeneralizationTest.Examples.lexicographicSelf (1 found):
  [apply] candidate 1/1: [Preorder α] → [LT α] [LE α]
    result: theorem lexicographicSelf_generalized {α : Type} [LT α] [LE α] {x y : α × α} :
    toLex x ≤ toLex y ↔ x.1 < y.1 ∨ x.1 = y.1 ∧ x.2 ≤ y.2
-/
#guard_msgs in
#autogeneralize lexicographicSelf

theorem lexicographicSelf_generalized {α : Type} [LT α] [LE α] {x y : α × α} :
    toLex x ≤ toLex y ↔ x.1 < y.1 ∨ x.1 = y.1 ∧ x.2 ≤ y.2 :=
  Prod.Lex.toLex_le_toLex

/-! ### Generalizing through a registered instance -/

/-
This wrapper deliberately strengthens Mathlib's `Semifield.isCoprime_iff` to
`Field`. Recovering `Semifield` makes the result usable for types such as `ℚ≥0`.
-/
theorem coprimeIffOverField {R : Type*} [Field R] {m n : R} :
    IsCoprime m n ↔ m ≠ 0 ∨ n ≠ 0 :=
  Semifield.isCoprime_iff

/--
info: Type class generalization candidates for AutoGeneralizationTest.Examples.coprimeIffOverField (1 found):
  [apply] candidate 1/1: [Field R] → [Semifield R]
    result: theorem coprimeIffOverField_generalized.{u_1} {R : Type u_1} [Semifield R] {m n : R} :
    IsCoprime m n ↔ m ≠ 0 ∨ n ≠ 0
-/
#guard_msgs in
#autogeneralize coprimeIffOverField

theorem coprimeIffOverField_generalized {R : Type*} [Semifield R] {m n : R} :
    IsCoprime m n ↔ m ≠ 0 ∨ n ≠ 0 :=
  Semifield.isCoprime_iff

example {m n : ℚ≥0} : IsCoprime m n ↔ m ≠ 0 ∨ n ≠ 0 :=
  coprimeIffOverField_generalized

/-
`StarRing R` stores lower algebraic evidence selected in the original `Field`
context. Re-synthesizing that evidence lets this proof keep `StarRing` while
weakening `Field` to `Semifield`.
-/
theorem selfAdjointDivOverField {R : Type*} [Field R] [StarRing R] {x y : R}
    (hx : IsSelfAdjoint x) (hy : IsSelfAdjoint y) : IsSelfAdjoint (x / y) :=
  IsSelfAdjoint.div hx hy

/--
info: Type class generalization candidates for AutoGeneralizationTest.Examples.selfAdjointDivOverField (1 found):
  [apply] candidate 1/1: [Field R] → [Semifield R]
    result: theorem selfAdjointDivOverField_generalized.{u_1} {R : Type u_1} [Semifield R] [StarRing R] {x y : R}
    (hx : IsSelfAdjoint x) (hy : IsSelfAdjoint y) : IsSelfAdjoint (x / y)
-/
#guard_msgs in
#autogeneralize selfAdjointDivOverField

theorem selfAdjointDivOverField_generalized {R : Type*} [Semifield R] [StarRing R]
    {x y : R} (hx : IsSelfAdjoint x) (hy : IsSelfAdjoint y) : IsSelfAdjoint (x / y) :=
  IsSelfAdjoint.div hx hy

/-! ### Generalizing every source -/

/-- With different component types, each `Preorder` supplies one required capability. -/
theorem lexicographicPair {α β : Type} [Preorder α] [Preorder β] {x y : α × β} :
    toLex x ≤ toLex y ↔ x.1 < y.1 ∨ x.1 = y.1 ∧ x.2 ≤ y.2 :=
  Prod.Lex.toLex_le_toLex

/--
info: Complete type class generalization for AutoGeneralizationTest.Examples.lexicographicPair (2 steps):
  [apply] step 1: [Preorder β] → [LE β]
  step 2: [Preorder α] → [LT α]
    result: theorem lexicographicPair_generalized {α β : Type} [LT α] [LE β] {x y : α × β} :
    toLex x ≤ toLex y ↔ x.1 < y.1 ∨ x.1 = y.1 ∧ x.2 ≤ y.2
-/
#guard_msgs in
#autogeneralize! lexicographicPair

theorem lexicographicPair_generalized {α β : Type} [LT α] [LE β] {x y : α × β} :
    toLex x ≤ toLex y ↔ x.1 < y.1 ∨ x.1 = y.1 ∧ x.2 ≤ y.2 :=
  Prod.Lex.toLex_le_toLex

/-! ### Replaying a type-class generalization from Mathlib -/

open Set Topology

/--
Before Mathlib PR #23193, `inv_mem_connectedComponent_one` used these stronger
`Group` and `IsTopologicalGroup` assumptions. The current theorem supplies the proof.
-/
theorem topologicalInvComponent {G : Type} [TopologicalSpace G] [Group G]
    [IsTopologicalGroup G] {g : G} (hg : g ∈ connectedComponent (1 : G)) :
    g⁻¹ ∈ connectedComponent (1 : G) :=
  inv_mem_connectedComponent_one hg

/--
info: Type class generalization candidates for AutoGeneralizationTest.Examples.topologicalInvComponent (1 found):
  [apply] candidate 1/1: [IsTopologicalGroup G] → [ContinuousInv G]
    result: theorem topologicalInvComponent_generalized {G : Type} [TopologicalSpace G] [Group G] [ContinuousInv G]
    {g : G} (hg : g ∈ connectedComponent 1) : g⁻¹ ∈ connectedComponent 1
-/
#guard_msgs in
#autogeneralize topologicalInvComponent

/--
info: Complete type class generalization for AutoGeneralizationTest.Examples.topologicalInvComponent (2 steps):
  [apply] step 1: [IsTopologicalGroup G] → [ContinuousInv G]
  step 2: [Group G] → [DivisionMonoid G]
    result: theorem topologicalInvComponent_generalized {G : Type} [TopologicalSpace G] [DivisionMonoid G]
    [ContinuousInv G] {g : G} (hg : g ∈ connectedComponent 1) : g⁻¹ ∈ connectedComponent 1
-/
#guard_msgs in
#autogeneralize! topologicalInvComponent

theorem topologicalInvComponent_generalized {G : Type} [TopologicalSpace G]
    [DivisionMonoid G] [ContinuousInv G] {g : G} (hg : g ∈ connectedComponent (1 : G)) :
    g⁻¹ ∈ connectedComponent (1 : G) :=
  inv_mem_connectedComponent_one hg

end AutoGeneralizationTest.Examples
end