harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Constructions/Cylinders.lean
theorem diff_cylinder_same (s : Finset ι) (S T : Set (∀ i : s, α i)) :
    cylinder s S \ cylinder s T = cylinder s (S \ T)

Proof state:
case h
ι : Type u_1
α : ι → Type u_2
s : Finset ι
S T : Set ((i : { x // x ∈ s }) → α ↑i)
f : (i : ι) → α i
⊢ f ∈ cylinder s S \ cylinder s T ↔ f ∈ cylinder s (S \ T)

Tactic:
simp only [mem_diff, mem_cylinder]

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
S T : Set ((i : { x // x ∈ s }) → α ↑i)
⊢ cylinder s S \ cylinder s T = cylinder s (S \ T)

Tactic:
ext1 f

Result:
case h
ι : Type u_1
α : ι → Type u_2
s : Finset ι
S T : Set ((i : { x // x ∈ s }) → α ↑i)
f : (i : ι) → α i
⊢ f ∈ cylinder s S \ cylinder s T ↔ f ∈ cylinder s (S \ T)
-- Mathlib/Data/Fin/Basic.lean
theorem mul_zero' [NeZero n] (k : Fin n) : k * 0 = 0

Proof state:
n : ℕ
inst✝ : NeZero n
k : Fin n
⊢ k * 0 = 0

Tactic:
simp [Fin.ext_iff, mul_def]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem div_right_injective : Function.Injective fun a ↦ b / a

Proof state:
G : Type u_3
inst✝ : Group G
b : G
⊢ Injective fun a => b * a⁻¹

Tactic:
exact fun a a' h ↦ inv_injective (mul_right_injective b h)

Result:
no goals

Proof state:
G : Type u_3
inst✝ : Group G
b : G
⊢ Injective fun a => b / a

Tactic:
simp only [div_eq_mul_inv]

Result:
G : Type u_3
inst✝ : Group G
b : G
⊢ Injective fun a => b * a⁻¹
-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem irreducible_pow_sup_of_le (hJ : Irreducible J) (n : ℕ) (hn : n ≤ emultiplicity J I) :
    J ^ n ⊔ I = J ^ n

Proof state:
case neg
T : Type u_4
inst✝¹ : CommRing T
inst✝ : IsDedekindDomain T
I J : Ideal T
hJ : Irreducible J
n : ℕ
hn : ↑n ≤ emultiplicity J I
hI : ¬I = ⊥
⊢ n ≤ count J (normalizedFactors I)

Tactic:
rw [emultiplicity_eq_count_normalizedFactors hJ hI, normalize_eq J] at hn

Result:
case neg
T : Type u_4
inst✝¹ : CommRing T
inst✝ : IsDedekindDomain T
I J : Ideal T
hJ : Irreducible J
n : ℕ
hn : ↑n ≤ ↑(count J (normalizedFactors I))
hI : ¬I = ⊥
⊢ n ≤ count J (normalizedFactors I)

Proof state:
case neg
T : Type u_4
inst✝¹ : CommRing T
inst✝ : IsDedekindDomain T
I J : Ideal T
hJ : Irreducible J
n : ℕ
hn : ↑n ≤ emultiplicity J I
hI : ¬I = ⊥
⊢ J ^ n ⊔ I = J ^ n

Tactic:
rw [irreducible_pow_sup hI hJ, min_eq_right]

Result:
case neg
T : Type u_4
inst✝¹ : CommRing T
inst✝ : IsDedekindDomain T
I J : Ideal T
hJ : Irreducible J
n : ℕ
hn : ↑n ≤ emultiplicity J I
hI : ¬I = ⊥
⊢ n ≤ count J (normalizedFactors I)

Proof state:
case pos
T : Type u_4
inst✝¹ : CommRing T
inst✝ : IsDedekindDomain T
I J : Ideal T
hJ : Irreducible J
n : ℕ
hn : ↑n ≤ emultiplicity J I
hI : I = ⊥
⊢ J ^ n ⊔ I = J ^ n

Tactic:
simp_all

Result:
no goals

Proof state:
T : Type u_4
inst✝¹ : CommRing T
inst✝ : IsDedekindDomain T
I J : Ideal T
hJ : Irreducible J
n : ℕ
hn : ↑n ≤ emultiplicity J I
⊢ J ^ n ⊔ I = J ^ n

Tactic:
by_cases hI : I = ⊥

Result:
case pos
T : Type u_4
inst✝¹ : CommRing T
inst✝ : IsDedekindDomain T
I J : Ideal T
hJ : Irreducible J
n : ℕ
hn : ↑n ≤ emultiplicity J I
hI : I = ⊥
⊢ J ^ n ⊔ I = J ^ n

case neg
T : Type u_4
inst✝¹ : CommRing T
inst✝ : IsDedekindDomain T
I J : Ideal T
hJ : Irreducible J
n : ℕ
hn : ↑n ≤ emultiplicity J I
hI : ¬I = ⊥
⊢ J ^ n ⊔ I = J ^ n

Proof state:
case neg
T : Type u_4
inst✝¹ : CommRing T
inst✝ : IsDedekindDomain T
I J : Ideal T
hJ : Irreducible J
n : ℕ
hn : ↑n ≤ ↑(count J (normalizedFactors I))
hI : ¬I = ⊥
⊢ n ≤ count J (normalizedFactors I)

Tactic:
exact_mod_cast hn

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Metric.lean
theorem edist_anti {G' : SimpleGraph V} (h : G ≤ G') :
    G'.edist u v ≤ G.edist u v

Proof state:
V : Type u_1
G : SimpleGraph V
u v : V
G' : SimpleGraph V
h : G ≤ G'
⊢ G'.edist u v ≤ G.edist u v

Tactic:
by_cases hr : G.Reachable u v

Result:
case pos
V : Type u_1
G : SimpleGraph V
u v : V
G' : SimpleGraph V
h : G ≤ G'
hr : G.Reachable u v
⊢ G'.edist u v ≤ G.edist u v

case neg
V : Type u_1
G : SimpleGraph V
u v : V
G' : SimpleGraph V
h : G ≤ G'
hr : ¬G.Reachable u v
⊢ G'.edist u v ≤ G.edist u v

Proof state:
case neg
V : Type u_1
G : SimpleGraph V
u v : V
G' : SimpleGraph V
h : G ≤ G'
hr : ¬G.Reachable u v
⊢ G'.edist u v ≤ G.edist u v

Tactic:
exact edist_eq_top_of_not_reachable hr ▸ le_top

Result:
no goals

Proof state:
case pos
V : Type u_1
G : SimpleGraph V
u v : V
G' : SimpleGraph V
h : G ≤ G'
hr : G.Reachable u v
⊢ G'.edist u v ≤ G.edist u v

Tactic:
obtain ⟨_, hw⟩ := hr.exists_walk_length_eq_edist

Result:
case pos.intro
V : Type u_1
G : SimpleGraph V
u v : V
G' : SimpleGraph V
h : G ≤ G'
hr : G.Reachable u v
w✝ : G.Walk u v
hw : ↑w✝.length = G.edist u v
⊢ G'.edist u v ≤ G.edist u v

Proof state:
case pos.intro
V : Type u_1
G : SimpleGraph V
u v : V
G' : SimpleGraph V
h : G ≤ G'
hr : G.Reachable u v
w✝ : G.Walk u v
hw : ↑w✝.length = G.edist u v
⊢ G'.edist u v ≤ G.edist u v

Tactic:
rw [← hw, ← Walk.length_map (Hom.mapSpanningSubgraphs h)]

Result:
case pos.intro
V : Type u_1
G : SimpleGraph V
u v : V
G' : SimpleGraph V
h : G ≤ G'
hr : G.Reachable u v
w✝ : G.Walk u v
hw : ↑w✝.length = G.edist u v
⊢ G'.edist u v ≤ ↑(Walk.map (Hom.mapSpanningSubgraphs h) w✝).length

Proof state:
case pos.intro
V : Type u_1
G : SimpleGraph V
u v : V
G' : SimpleGraph V
h : G ≤ G'
hr : G.Reachable u v
w✝ : G.Walk u v
hw : ↑w✝.length = G.edist u v
⊢ G'.edist u v ≤ ↑(Walk.map (Hom.mapSpanningSubgraphs h) w✝).length

Tactic:
apply edist_le

Result:
no goals
-- Mathlib/NumberTheory/EllipticDivisibilitySequence.lean
@[simp]
lemma preNormEDS_three : preNormEDS b c d 3 = c

Proof state:
R : Type u
inst✝ : CommRing R
b c d : R
⊢ preNormEDS b c d 3 = c

Tactic:
erw [preNormEDS_ofNat, preNormEDS'_three]

Result:
no goals
-- Mathlib/Computability/PostTuringMachine.lean
theorem univ_supports (M : Machine Γ Λ) : Supports M Set.univ

Proof state:
Γ : Type u_1
Λ : Type u_2
inst✝ : Inhabited Λ
M : Machine Γ Λ
⊢ Supports M Set.univ

Tactic:
constructor <;> intros <;> apply Set.mem_univ

Result:
no goals
-- Mathlib/Algebra/Homology/DerivedCategory/Ext/Basic.lean
@[simp]
lemma comp_assoc_of_second_deg_zero
    {a₁ a₃ a₁₃ : ℕ} (α : Ext X Y a₁) (β : Ext Y Z 0) (γ : Ext Z T a₃)
    (h₁₃ : a₁ + a₃ = a₁₃) :
    (α.comp β (add_zero _)).comp γ h₁₃ = α.comp (β.comp γ (zero_add _)) h₁₃

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z T : C
a₁ a₃ a₁₃ : ℕ
α : Ext X Y a₁
β : Ext Y Z 0
γ : Ext Z T a₃
h₁₃ : a₁ + a₃ = a₁₃
⊢ (α.comp β ⋯).comp γ h₁₃ = α.comp (β.comp γ ⋯) h₁₃

Tactic:
apply comp_assoc

Result:
case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z T : C
a₁ a₃ a₁₃ : ℕ
α : Ext X Y a₁
β : Ext Y Z 0
γ : Ext Z T a₃
h₁₃ : a₁ + a₃ = a₁₃
⊢ a₁ + 0 + a₃ = a₁₃

Proof state:
case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z T : C
a₁ a₃ a₁₃ : ℕ
α : Ext X Y a₁
β : Ext Y Z 0
γ : Ext Z T a₃
h₁₃ : a₁ + a₃ = a₁₃
⊢ a₁ + 0 + a₃ = a₁₃

Tactic:
omega

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
@[reassoc (attr := simp), elementwise (attr := simp)]
lemma isoTwoCocycles_hom_comp_subtype :
    (isoTwoCocycles A).hom ≫ ModuleCat.ofHom (twoCocycles A).subtype =
      iCocycles A 2 ≫ (twoCochainsLequiv A).toModuleIso.hom

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
this :
  (shortComplexH2 A).moduleCatCyclesIso.hom ≫
      ModuleCat.ofHom (LinearMap.ker (ModuleCat.Hom.hom (shortComplexH2 A).g)).subtype =
    (shortComplexH2 A).iCycles
⊢ (isoTwoCocycles A).hom ≫ ModuleCat.ofHom (twoCocycles A).subtype =
    iCocycles A 2 ≫ (twoCochainsLequiv A).toModuleIso.hom

Tactic:
simp_all [shortComplexH2, isoTwoCocycles, twoCocycles]

Result:
no goals

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (isoTwoCocycles A).hom ≫ ModuleCat.ofHom (twoCocycles A).subtype =
    iCocycles A 2 ≫ (twoCochainsLequiv A).toModuleIso.hom

Tactic:
have := (shortComplexH2 A).moduleCatCyclesIso_hom_subtype

Result:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
this :
  (shortComplexH2 A).moduleCatCyclesIso.hom ≫
      ModuleCat.ofHom (LinearMap.ker (ModuleCat.Hom.hom (shortComplexH2 A).g)).subtype =
    (shortComplexH2 A).iCycles
⊢ (isoTwoCocycles A).hom ≫ ModuleCat.ofHom (twoCocycles A).subtype =
    iCocycles A 2 ≫ (twoCochainsLequiv A).toModuleIso.hom
-- Mathlib/CategoryTheory/Functor/Flat.lean
theorem fac (x : J) : lift F hc s ≫ (F.mapCone c).π.app x = s.π.app x

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K : J ⥤ C
F : C ⥤ D
inst✝ : RepresentablyFlat F
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
x : J
⊢ lift F hc s ≫ (F.mapCone c).π.app x = s.π.app x

Tactic:
simp [lift, ← Functor.map_comp]

Result:
no goals
-- Mathlib/Data/Nat/Choose/Basic.lean
theorem multichoose_eq : ∀ n k : ℕ, multichoose n k = (n + k - 1).choose k
  | _, 0 => by simp
  | 0, k + 1 => by simp
  | n + 1, k + 1 => by
    have : n + (k + 1) < (n + 1) + (k + 1) := Nat.add_lt_add_right (Nat.lt_succ_self _) _
    have : (n + 1) + k < (n + 1) + (k + 1) := Nat.add_lt_add_left (Nat.lt_succ_self _) _
    rw [multichoose_succ_succ, Nat.add_comm, Nat.succ_add_sub_one, ← Nat.add_assoc,
      Nat.choose_succ_succ]
    simp [multichoose_eq n (k+1), multichoose_eq (n+1) k]

Proof state:
k : ℕ
⊢ multichoose 0 (k + 1) = (0 + (k + 1) - 1).choose (k + 1)

Tactic:
simp

Result:
no goals

Proof state:
n k : ℕ
⊢ (n + 1).multichoose (k + 1) = (n + 1 + (k + 1) - 1).choose (k + 1)

Tactic:
have : n + (k + 1) < (n + 1) + (k + 1) := Nat.add_lt_add_right (Nat.lt_succ_self _) _

Result:
n k : ℕ
this : n + (k + 1) < n + 1 + (k + 1)
⊢ (n + 1).multichoose (k + 1) = (n + 1 + (k + 1) - 1).choose (k + 1)

Proof state:
x✝ : ℕ
⊢ x✝.multichoose 0 = (x✝ + 0 - 1).choose 0

Tactic:
simp

Result:
no goals

Proof state:
n k : ℕ
this✝ : n + (k + 1) < n + 1 + (k + 1)
this : n + 1 + k < n + 1 + (k + 1)
⊢ (n + 1).multichoose k + n.multichoose (k + 1) = (n + k).choose k + (n + k).choose k.succ

Tactic:
simp [multichoose_eq n (k+1), multichoose_eq (n+1) k]

Result:
no goals

Proof state:
n k : ℕ
this : n + (k + 1) < n + 1 + (k + 1)
⊢ (n + 1).multichoose (k + 1) = (n + 1 + (k + 1) - 1).choose (k + 1)

Tactic:
have : (n + 1) + k < (n + 1) + (k + 1) := Nat.add_lt_add_left (Nat.lt_succ_self _) _

Result:
n k : ℕ
this✝ : n + (k + 1) < n + 1 + (k + 1)
this : n + 1 + k < n + 1 + (k + 1)
⊢ (n + 1).multichoose (k + 1) = (n + 1 + (k + 1) - 1).choose (k + 1)

Proof state:
n k : ℕ
this✝ : n + (k + 1) < n + 1 + (k + 1)
this : n + 1 + k < n + 1 + (k + 1)
⊢ (n + 1).multichoose (k + 1) = (n + 1 + (k + 1) - 1).choose (k + 1)

Tactic:
rw [multichoose_succ_succ, Nat.add_comm, Nat.succ_add_sub_one, ← Nat.add_assoc,
  Nat.choose_succ_succ]

Result:
n k : ℕ
this✝ : n + (k + 1) < n + 1 + (k + 1)
this : n + 1 + k < n + 1 + (k + 1)
⊢ (n + 1).multichoose k + n.multichoose (k + 1) = (n + k).choose k + (n + k).choose k.succ
-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem mem_div_iff_of_nonzero {I J : FractionalIdeal R₁⁰ K} (h : J ≠ 0) {x} :
    x ∈ I / J ↔ ∀ y ∈ J, x * y ∈ I

Proof state:
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I J : FractionalIdeal R₁⁰ K
h : J ≠ 0
x : K
⊢ x ∈ I / J ↔ ∀ y ∈ J, x * y ∈ I

Tactic:
rw [div_nonzero h]

Result:
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I J : FractionalIdeal R₁⁰ K
h : J ≠ 0
x : K
⊢ x ∈ ⟨↑I / ↑J, ⋯⟩ ↔ ∀ y ∈ J, x * y ∈ I

Proof state:
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I J : FractionalIdeal R₁⁰ K
h : J ≠ 0
x : K
⊢ x ∈ ⟨↑I / ↑J, ⋯⟩ ↔ ∀ y ∈ J, x * y ∈ I

Tactic:
exact Submodule.mem_div_iff_forall_mul_mem

Result:
no goals
-- Mathlib/Algebra/Lie/OfAssociative.lean
lemma toEnd_pow_comp_lieHom :
    (toEnd R L M₂ x ^ k) ∘ₗ f = f ∘ₗ toEnd R L M x ^ k

Proof state:
case h.h
R : Type u
L : Type v
M : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
M₂ : Type w₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
f : M →ₗ⁅R,L⁆ M₂
k : ℕ
x : L
x✝ : M
⊢ ((toEnd R L M₂) x ∘ₗ ↑f) x✝ = (↑f ∘ₗ (toEnd R L M) x) x✝

Tactic:
simp

Result:
no goals

Proof state:
case h
R : Type u
L : Type v
M : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
M₂ : Type w₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
f : M →ₗ⁅R,L⁆ M₂
k : ℕ
x : L
⊢ (toEnd R L M₂) x ∘ₗ ↑f = ↑f ∘ₗ (toEnd R L M) x

Tactic:
ext

Result:
case h.h
R : Type u
L : Type v
M : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
M₂ : Type w₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
f : M →ₗ⁅R,L⁆ M₂
k : ℕ
x : L
x✝ : M
⊢ ((toEnd R L M₂) x ∘ₗ ↑f) x✝ = (↑f ∘ₗ (toEnd R L M) x) x✝

Proof state:
R : Type u
L : Type v
M : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
M₂ : Type w₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
f : M →ₗ⁅R,L⁆ M₂
k : ℕ
x : L
⊢ ((toEnd R L M₂) x ^ k) ∘ₗ ↑f = ↑f ∘ₗ (toEnd R L M) x ^ k

Tactic:
apply LinearMap.commute_pow_left_of_commute

Result:
case h
R : Type u
L : Type v
M : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
M₂ : Type w₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
f : M →ₗ⁅R,L⁆ M₂
k : ℕ
x : L
⊢ (toEnd R L M₂) x ∘ₗ ↑f = ↑f ∘ₗ (toEnd R L M) x
-- Mathlib/AlgebraicGeometry/Scheme.lean
theorem basicOpen_eq_of_affine' {R : CommRingCat} (f : Γ(Spec R, ⊤)) :
    (Spec R).basicOpen f = PrimeSpectrum.basicOpen ((Scheme.ΓSpecIso R).hom f)

Proof state:
R : CommRingCat
f : ↑Γ(Spec R, ⊤)
⊢ (Spec R).basicOpen f = PrimeSpectrum.basicOpen ((ConcreteCategory.hom (Scheme.ΓSpecIso R).hom) f)

Tactic:
convert basicOpen_eq_of_affine ((Scheme.ΓSpecIso R).hom f)

Result:
case h.e'_2.h.e'_3
R : CommRingCat
f : ↑Γ(Spec R, ⊤)
⊢ f = (ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) ((ConcreteCategory.hom (Scheme.ΓSpecIso R).hom) f)

Proof state:
case h.e'_2.h.e'_3
R : CommRingCat
f : ↑Γ(Spec R, ⊤)
⊢ f = (ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) ((ConcreteCategory.hom (Scheme.ΓSpecIso R).hom) f)

Tactic:
exact (Iso.hom_inv_id_apply (Scheme.ΓSpecIso R) f).symm

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem imp_eq_of_eq_true_left {a b : Prop} (h : a = True) : (a → b) = b

Proof state:
a b : Prop
h : a = True
⊢ (a → b) = b

Tactic:
simp [h]

Result:
no goals
-- Mathlib/RingTheory/RootsOfUnity/Basic.lean
theorem map_rootsOfUnity_eq_pow_self [FunLike F R R] [RingHomClass F R R] (σ : F)
    (ζ : rootsOfUnity k R) :
    ∃ m : ℕ, σ (ζ : Rˣ) = ((ζ : Rˣ) : R) ^ m

Proof state:
case intro
R : Type u_4
F : Type u_6
k : ℕ
inst✝⁴ : NeZero k
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : FunLike F R R
inst✝ : RingHomClass F R R
σ : F
ζ : ↥(rootsOfUnity k R)
m : ℤ
hm : ∀ (g : ↥(rootsOfUnity k R)), (restrictRootsOfUnity σ k) g = g ^ m
⊢ ∃ m, σ ↑↑ζ = ↑↑ζ ^ m

Tactic:
rw [← restrictRootsOfUnity_coe_apply, hm, ← zpow_mod_orderOf, ← Int.toNat_of_nonneg
    (m.emod_nonneg (Int.natCast_ne_zero.mpr (pos_iff_ne_zero.mp (orderOf_pos ζ)))),
  zpow_natCast, rootsOfUnity.coe_pow]

Result:
case intro
R : Type u_4
F : Type u_6
k : ℕ
inst✝⁴ : NeZero k
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : FunLike F R R
inst✝ : RingHomClass F R R
σ : F
ζ : ↥(rootsOfUnity k R)
m : ℤ
hm : ∀ (g : ↥(rootsOfUnity k R)), (restrictRootsOfUnity σ k) g = g ^ m
⊢ ∃ m_1, ↑↑ζ ^ (m % ↑(orderOf ζ)).toNat = ↑↑ζ ^ m_1

Proof state:
case intro
R : Type u_4
F : Type u_6
k : ℕ
inst✝⁴ : NeZero k
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : FunLike F R R
inst✝ : RingHomClass F R R
σ : F
ζ : ↥(rootsOfUnity k R)
m : ℤ
hm : ∀ (g : ↥(rootsOfUnity k R)), (restrictRootsOfUnity σ k) g = g ^ m
⊢ ∃ m_1, ↑↑ζ ^ (m % ↑(orderOf ζ)).toNat = ↑↑ζ ^ m_1

Tactic:
exact ⟨(m % orderOf ζ).toNat, rfl⟩

Result:
no goals

Proof state:
R : Type u_4
F : Type u_6
k : ℕ
inst✝⁴ : NeZero k
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : FunLike F R R
inst✝ : RingHomClass F R R
σ : F
ζ : ↥(rootsOfUnity k R)
⊢ ∃ m, σ ↑↑ζ = ↑↑ζ ^ m

Tactic:
obtain ⟨m, hm⟩ := MonoidHom.map_cyclic (restrictRootsOfUnity σ k)

Result:
case intro
R : Type u_4
F : Type u_6
k : ℕ
inst✝⁴ : NeZero k
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : FunLike F R R
inst✝ : RingHomClass F R R
σ : F
ζ : ↥(rootsOfUnity k R)
m : ℤ
hm : ∀ (g : ↥(rootsOfUnity k R)), (restrictRootsOfUnity σ k) g = g ^ m
⊢ ∃ m, σ ↑↑ζ = ↑↑ζ ^ m
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Ico_subset_Iio_self : Ico a b ⊆ Iio b

Proof state:
α : Type u_2
a b : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : LocallyFiniteOrder α
⊢ Ico a b ⊆ Iio b

Tactic:
simpa [← coe_subset] using Set.Ico_subset_Iio_self

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean
theorem card_pos_of_affineSpan_eq_top {ι : Type*} [Fintype ι] {p : ι → P}
    (h : affineSpan k (range p) = ⊤) : 0 < Fintype.card ι

Proof state:
case intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
inst✝ : Fintype ι
p : ι → P
h : affineSpan k (range p) = ⊤
i : ι
⊢ 0 < Fintype.card ι

Tactic:
exact Fintype.card_pos_iff.mpr ⟨i⟩

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
inst✝ : Fintype ι
p : ι → P
h : affineSpan k (range p) = ⊤
⊢ 0 < Fintype.card ι

Tactic:
obtain ⟨-, ⟨i, -⟩⟩ := nonempty_of_affineSpan_eq_top k V P h

Result:
case intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
inst✝ : Fintype ι
p : ι → P
h : affineSpan k (range p) = ⊤
i : ι
⊢ 0 < Fintype.card ι
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem lt_sub_of_add_lt {a b c : Nat} (h : a + b < c) : a < c - b :=
  have : a.succ + b ≤ c

Proof state:
a b c : Nat
h : a + b < c
⊢ a + b + 1 ≤ c

Tactic:
exact h

Result:
no goals

Proof state:
a b c : Nat
h : a + b < c
⊢ a.succ + b ≤ c

Tactic:
simp [Nat.succ_add]

Result:
a b c : Nat
h : a + b < c
⊢ a + b + 1 ≤ c
-- Mathlib/Order/Radical.lean
theorem Order.radical_nongenerating [IsCoatomic α] {a : α} (h : a ⊔ radical α = ⊤) : a = ⊤

Proof state:
case inr.intro.intro
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : IsCoatomic α
a : α
h : a ⊔ radical α = ⊤
m : α
c : IsCoatom m
le : a ≤ m
q : a ⊔ radical α ≤ m
⊢ a = ⊤

Tactic:
rw [h, top_le_iff] at q

Result:
case inr.intro.intro
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : IsCoatomic α
a : α
h : a ⊔ radical α = ⊤
m : α
c : IsCoatom m
le : a ≤ m
q : m = ⊤
⊢ a = ⊤

Proof state:
case inr
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : IsCoatomic α
a : α
h : a ⊔ radical α = ⊤
w : ∃ a_1, IsCoatom a_1 ∧ a ≤ a_1
⊢ a = ⊤

Tactic:
obtain ⟨m, c, le⟩ := w

Result:
case inr.intro.intro
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : IsCoatomic α
a : α
h : a ⊔ radical α = ⊤
m : α
c : IsCoatom m
le : a ≤ m
⊢ a = ⊤

Proof state:
case inr.intro.intro
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : IsCoatomic α
a : α
h : a ⊔ radical α = ⊤
m : α
c : IsCoatom m
le : a ≤ m
q : m = ⊤
⊢ a = ⊤

Tactic:
simpa using c.1 q

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : IsCoatomic α
a : α
h : a ⊔ radical α = ⊤
⊢ a = ⊤

Tactic:
obtain (rfl | w) := eq_top_or_exists_le_coatom a

Result:
case inl
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : IsCoatomic α
h : ⊤ ⊔ radical α = ⊤
⊢ ⊤ = ⊤

case inr
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : IsCoatomic α
a : α
h : a ⊔ radical α = ⊤
w : ∃ a_1, IsCoatom a_1 ∧ a ≤ a_1
⊢ a = ⊤

Proof state:
case inr.intro.intro
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : IsCoatomic α
a : α
h : a ⊔ radical α = ⊤
m : α
c : IsCoatom m
le : a ≤ m
⊢ a = ⊤

Tactic:
have q : a ⊔ radical α ≤ m := sup_le le (radical_le_coatom c)

Result:
case inr.intro.intro
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : IsCoatomic α
a : α
h : a ⊔ radical α = ⊤
m : α
c : IsCoatom m
le : a ≤ m
q : a ⊔ radical α ≤ m
⊢ a = ⊤

Proof state:
case inl
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : IsCoatomic α
h : ⊤ ⊔ radical α = ⊤
⊢ ⊤ = ⊤

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Asymptotics/SpecificAsymptotics.lean
theorem tendsto_pow_div_pow_atTop_atTop {p q : ℕ} (hpq : q < p) :
    Tendsto (fun x : 𝕜 => x ^ p / x ^ q) atTop atTop

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p q : ℕ
hpq : q < p
⊢ Tendsto (fun x => x ^ p / x ^ q) atTop atTop

Tactic:
rw [tendsto_congr' pow_div_pow_eventuallyEq_atTop]

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p q : ℕ
hpq : q < p
⊢ Tendsto (fun x => x ^ (↑p - ↑q)) atTop atTop

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p q : ℕ
hpq : q < p
⊢ Tendsto (fun x => x ^ (↑p - ↑q)) atTop atTop

Tactic:
apply tendsto_zpow_atTop_atTop

Result:
case hn
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p q : ℕ
hpq : q < p
⊢ 0 < ↑p - ↑q

Proof state:
case hn
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p q : ℕ
hpq : q < p
⊢ 0 < ↑p - ↑q

Tactic:
omega

Result:
no goals
-- Mathlib/Data/Finset/Grade.lean
/-- Finsets form an order-connected suborder of multisets. -/
lemma ordConnected_range_val : Set.OrdConnected (Set.range val : Set <| Multiset α) :=
  ⟨by rintro _ _ _ ⟨s, rfl⟩ t ht; exact ⟨⟨t, Multiset.nodup_of_le ht.2 s.2⟩, rfl⟩⟩

Proof state:
case intro
α : Type u_1
x✝ : Multiset α
hx✝ : x✝ ∈ Set.range val
s : Finset α
t : Multiset α
ht : t ∈ Set.Icc x✝ s.val
⊢ t ∈ Set.range val

Tactic:
exact ⟨⟨t, Multiset.nodup_of_le ht.2 s.2⟩, rfl⟩

Result:
no goals

Proof state:
α : Type u_1
⊢ ∀ ⦃x : Multiset α⦄, x ∈ Set.range val → ∀ ⦃y : Multiset α⦄, y ∈ Set.range val → Set.Icc x y ⊆ Set.range val

Tactic:
rintro _ _ _ ⟨s, rfl⟩ t ht

Result:
case intro
α : Type u_1
x✝ : Multiset α
hx✝ : x✝ ∈ Set.range val
s : Finset α
t : Multiset α
ht : t ∈ Set.Icc x✝ s.val
⊢ t ∈ Set.range val
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem padicValInt_dvd (a : ℤ) : (p : ℤ) ^ padicValInt p a ∣ a

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
a : ℤ
⊢ ↑p ^ padicValInt p a ∣ a

Tactic:
rw [padicValInt_dvd_iff]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
a : ℤ
⊢ a = 0 ∨ padicValInt p a ≤ padicValInt p a

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
a : ℤ
⊢ a = 0 ∨ padicValInt p a ≤ padicValInt p a

Tactic:
exact Or.inr le_rfl

Result:
no goals
-- Mathlib/Algebra/Pointwise/Stabilizer.lean
@[to_additive (attr := simp, norm_cast)]
lemma stabilizer_coe_finset (s : Finset α) : stabilizer G (s : Set α) = stabilizer G s

Proof state:
G : Type u_1
α : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : DecidableEq α
s : Finset α
⊢ stabilizer G ↑s = stabilizer G s

Tactic:
ext

Result:
case h
G : Type u_1
α : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : DecidableEq α
s : Finset α
x✝ : G
⊢ x✝ ∈ stabilizer G ↑s ↔ x✝ ∈ stabilizer G s

Proof state:
case h
G : Type u_1
α : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : DecidableEq α
s : Finset α
x✝ : G
⊢ x✝ ∈ stabilizer G ↑s ↔ x✝ ∈ stabilizer G s

Tactic:
simp [← Finset.coe_inj]

Result:
no goals
-- Mathlib/Data/Fintype/Sets.lean
theorem toFinset_ssubset [Fintype s] {t : Finset α} : s.toFinset ⊂ t ↔ s ⊂ t

Proof state:
α : Type u_1
s : Set α
inst✝ : Fintype ↑s
t : Finset α
⊢ s.toFinset ⊂ t ↔ s ⊂ ↑t

Tactic:
rw [← Finset.coe_ssubset, coe_toFinset]

Result:
no goals