harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Order/DenselyOrdered.lean
theorem isClosed_Ico_iff {a b : α} : IsClosed (Set.Ico a b) ↔ b ≤ a

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
h : IsClosed (Ico a b)
hab : a < b
⊢ False

Tactic:
have := h.closure_eq

Result:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
h : IsClosed (Ico a b)
hab : a < b
this : closure (Ico a b) = Ico a b
⊢ False

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
⊢ IsClosed (Ico a b) ↔ b ≤ a

Tactic:
refine ⟨fun h => le_of_not_lt fun hab => ?_, by simp_all⟩

Result:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
h : IsClosed (Ico a b)
hab : a < b
⊢ False

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
h : IsClosed (Ico a b)
hab : a < b
this : ¬a ≤ b
⊢ False

Tactic:
exact this hab.le

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
⊢ b ≤ a → IsClosed (Ico a b)

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
h : IsClosed (Ico a b)
hab : a < b
this : closure (Ico a b) = Ico a b
⊢ False

Tactic:
rw [closure_Ico hab.ne, Icc_eq_Ico_same_iff] at this

Result:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
h : IsClosed (Ico a b)
hab : a < b
this : ¬a ≤ b
⊢ False
-- Mathlib/CategoryTheory/Closed/Ideal.lean
theorem ExponentialIdeal.mk_of_iso [Reflective i]
    (h : ∀ A : C, i ⋙ exp A ⋙ reflector i ⋙ i ≅ i ⋙ exp A) : ExponentialIdeal i

Proof state:
C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝² : ChosenFiniteProducts C
inst✝¹ : CartesianClosed C
inst✝ : Reflective i
h : (A : C) → i ⋙ exp A ⋙ reflector i ⋙ i ≅ i ⋙ exp A
⊢ ExponentialIdeal i

Tactic:
apply ExponentialIdeal.mk'

Result:
case h
C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝² : ChosenFiniteProducts C
inst✝¹ : CartesianClosed C
inst✝ : Reflective i
h : (A : C) → i ⋙ exp A ⋙ reflector i ⋙ i ≅ i ⋙ exp A
⊢ ∀ (B : D) (A : C), i.essImage (A ⟹ i.obj B)

Proof state:
case h
C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝² : ChosenFiniteProducts C
inst✝¹ : CartesianClosed C
inst✝ : Reflective i
h : (A : C) → i ⋙ exp A ⋙ reflector i ⋙ i ≅ i ⋙ exp A
B : D
A : C
⊢ i.essImage (A ⟹ i.obj B)

Tactic:
exact ⟨_, ⟨(h A).app B⟩⟩

Result:
no goals

Proof state:
case h
C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝² : ChosenFiniteProducts C
inst✝¹ : CartesianClosed C
inst✝ : Reflective i
h : (A : C) → i ⋙ exp A ⋙ reflector i ⋙ i ≅ i ⋙ exp A
⊢ ∀ (B : D) (A : C), i.essImage (A ⟹ i.obj B)

Tactic:
intro B A

Result:
case h
C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝² : ChosenFiniteProducts C
inst✝¹ : CartesianClosed C
inst✝ : Reflective i
h : (A : C) → i ⋙ exp A ⋙ reflector i ⋙ i ≅ i ⋙ exp A
B : D
A : C
⊢ i.essImage (A ⟹ i.obj B)
-- Mathlib/Data/Matroid/Constructions.lean
theorem freeOn_empty (α : Type*) : freeOn (∅ : Set α) = emptyOn α

Proof state:
α : Type u_2
⊢ freeOn ∅ = emptyOn α

Tactic:
simp [freeOn]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@[simp]
lemma ofHoms_zero : ofHoms (fun p => (0 : F.X p ⟶ G.X p)) = 0

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
⊢ (ofHoms fun p => 0) = 0

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/AlgebraicGeometry/Modules/Tilde.lean
lemma smul_stalk_no_nonzero_divisor {x : PrimeSpectrum R}
    (r : x.asIdeal.primeCompl) (st : (tildeInModuleCat M).stalk x) (hst : r.1 • st = 0) :
    st = 0

Proof state:
R : Type u
inst✝ : CommRing R
M : ModuleCat R
x : PrimeSpectrum R
r : ↥x.asIdeal.primeCompl
st : ↑(M.tildeInModuleCat.stalk x)
hst : ↑r • st = 0
U : (OpenNhds x)ᵒᵖ
i : op { obj := PrimeSpectrum.basicOpen ↑r, property := ⋯ } ⟶ U
s :
  ↑((((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑(PrimeSpectrum.Top R))ᵒᵖ (ModuleCat R)).obj (OpenNhds.inclusion x).op).obj
          M.tildeInModuleCat).obj
      U)
hs : ↑r • s = 0
pt : ↥(unop ((OpenNhds.inclusion x).op.obj U))
⊢ ↑s pt = ↑0 pt

Tactic:
apply LocalizedModule.eq_zero_of_smul_eq_zero _ (i.unop pt).2 _
  (congr_fun (Subtype.ext_iff.1 hs) pt)

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
M : ModuleCat R
x : PrimeSpectrum R
r : ↥x.asIdeal.primeCompl
st : ↑(M.tildeInModuleCat.stalk x)
hst : ↑r • st = 0
⊢ st = 0

Tactic:
refine Limits.Concrete.colimit_no_zero_smul_divisor
  _ _ _ ⟨op ⟨PrimeSpectrum.basicOpen r.1, r.2⟩, fun U i s hs ↦ Subtype.eq <| funext fun pt ↦ ?_⟩
  _ hst

Result:
R : Type u
inst✝ : CommRing R
M : ModuleCat R
x : PrimeSpectrum R
r : ↥x.asIdeal.primeCompl
st : ↑(M.tildeInModuleCat.stalk x)
hst : ↑r • st = 0
U : (OpenNhds x)ᵒᵖ
i : op { obj := PrimeSpectrum.basicOpen ↑r, property := ⋯ } ⟶ U
s :
  ↑((((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑(PrimeSpectrum.Top R))ᵒᵖ (ModuleCat R)).obj (OpenNhds.inclusion x).op).obj
          M.tildeInModuleCat).obj
      U)
hs : ↑r • s = 0
pt : ↥(unop ((OpenNhds.inclusion x).op.obj U))
⊢ ↑s pt = ↑0 pt
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem cons_msb_setWidth (x : BitVec (w+1)) : (cons x.msb (x.setWidth w)) = x

Proof state:
case pred
w : Nat
x : BitVec (w + 1)
i : Nat
a✝ : i < w + 1
⊢ (if i = w then x.msb else (setWidth w x).getLsbD i) = x.getLsbD i

Tactic:
split <;> rename_i h

Result:
case pred.isTrue
w : Nat
x : BitVec (w + 1)
i : Nat
a✝ : i < w + 1
h : i = w
⊢ x.msb = x.getLsbD i

case pred.isFalse
w : Nat
x : BitVec (w + 1)
i : Nat
a✝ : i < w + 1
h : ¬i = w
⊢ (setWidth w x).getLsbD i = x.getLsbD i

Proof state:
case pred.isTrue
w : Nat
x : BitVec (w + 1)
i : Nat
a✝ : i < w + 1
h : i = w
⊢ x.msb = x.getLsbD i

Tactic:
simp [BitVec.msb, getMsbD, h]

Result:
no goals

Proof state:
w : Nat
x : BitVec (w + 1)
⊢ cons x.msb (setWidth w x) = x

Tactic:
ext i

Result:
case pred
w : Nat
x : BitVec (w + 1)
i : Nat
a✝ : i < w + 1
⊢ (cons x.msb (setWidth w x)).getLsbD i = x.getLsbD i

Proof state:
case pred
w : Nat
x : BitVec (w + 1)
i : Nat
a✝ : i < w + 1
⊢ (cons x.msb (setWidth w x)).getLsbD i = x.getLsbD i

Tactic:
simp only [getLsbD_cons]

Result:
case pred
w : Nat
x : BitVec (w + 1)
i : Nat
a✝ : i < w + 1
⊢ (if i = w then x.msb else (setWidth w x).getLsbD i) = x.getLsbD i

Proof state:
case neg
w : Nat
x : BitVec (w + 1)
i : Nat
a✝ : i < w + 1
h : ¬i = w
h' : ¬i < w
⊢ (setWidth w x).getLsbD i = x.getLsbD i

Tactic:
omega

Result:
no goals

Proof state:
case pred.isFalse
w : Nat
x : BitVec (w + 1)
i : Nat
a✝ : i < w + 1
h : ¬i = w
⊢ (setWidth w x).getLsbD i = x.getLsbD i

Tactic:
by_cases h' : i < w

Result:
case pos
w : Nat
x : BitVec (w + 1)
i : Nat
a✝ : i < w + 1
h : ¬i = w
h' : i < w
⊢ (setWidth w x).getLsbD i = x.getLsbD i

case neg
w : Nat
x : BitVec (w + 1)
i : Nat
a✝ : i < w + 1
h : ¬i = w
h' : ¬i < w
⊢ (setWidth w x).getLsbD i = x.getLsbD i

Proof state:
case pos
w : Nat
x : BitVec (w + 1)
i : Nat
a✝ : i < w + 1
h : ¬i = w
h' : i < w
⊢ (setWidth w x).getLsbD i = x.getLsbD i

Tactic:
simp_all

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
theorem hasFTaylorSeriesUpTo_iteratedFDeriv :
    HasFTaylorSeriesUpTo ⊤ f (fun v n ↦ f.iteratedFDeriv n v)

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
n : ℕ
x : (i : ι) → E i
H :
  (f.iteratedFDeriv n.succ x).curryLeft =
    ∑ e : Fin n ↪ ι,
      ((f.iteratedFDerivComponent e.toEquivRange).linearDeriv ((Pi.compRightL 𝕜 E Subtype.val) x)).comp
        (Pi.compRightL 𝕜 E Subtype.val)
⊢ HasFDerivAt (fun y => f.iteratedFDeriv n y) (f.iteratedFDeriv n.succ x).curryLeft x

Tactic:
have A : HasFDerivAt (f.iteratedFDeriv n) (∑ e : Fin n ↪ ι,
    ((iteratedFDerivComponent f e.toEquivRange).linearDeriv (Pi.compRightL 𝕜 _ Subtype.val x))
      ∘L (Pi.compRightL 𝕜 _ Subtype.val)) x := by
  apply HasFDerivAt.sum (fun s _hs ↦ ?_)
  exact (ContinuousMultilinearMap.hasFDerivAt _ _).comp x (ContinuousLinearMap.hasFDerivAt _)

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
n : ℕ
x : (i : ι) → E i
H :
  (f.iteratedFDeriv n.succ x).curryLeft =
    ∑ e : Fin n ↪ ι,
      ((f.iteratedFDerivComponent e.toEquivRange).linearDeriv ((Pi.compRightL 𝕜 E Subtype.val) x)).comp
        (Pi.compRightL 𝕜 E Subtype.val)
A :
  HasFDerivAt (f.iteratedFDeriv n)
    (∑ e : Fin n ↪ ι,
      ((f.iteratedFDerivComponent e.toEquivRange).linearDeriv ((Pi.compRightL 𝕜 E Subtype.val) x)).comp
        (Pi.compRightL 𝕜 E Subtype.val))
    x
⊢ HasFDerivAt (fun y => f.iteratedFDeriv n y) (f.iteratedFDeriv n.succ x).curryLeft x
-- Mathlib/Order/JordanHolder.lean
theorem isMaximal_eraseLast_last {s : CompositionSeries X} (h : 0 < s.length) :
    IsMaximal s.eraseLast.last s.last

Proof state:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
this : s.length - 1 + 1 = s.length
⊢ IsMaximal (s.toFun ⟨s.length.pred, ⋯⟩) (s.toFun (Fin.last s.length))

Tactic:
convert s.step ⟨s.length - 1, by omega⟩

Result:
case h.e'_5.h.e'_4
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
this : s.length - 1 + 1 = s.length
⊢ Fin.last s.length = ⟨s.length - 1, ⋯⟩.succ

Proof state:
case h.e'_5.h.e'_4
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
this : s.length - 1 + 1 = s.length
⊢ Fin.last s.length = ⟨s.length - 1, ⋯⟩.succ

Tactic:
ext

Result:
case h.e'_5.h.e'_4.h
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
this : s.length - 1 + 1 = s.length
⊢ ↑(Fin.last s.length) = ↑⟨s.length - 1, ⋯⟩.succ

Proof state:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
⊢ IsMaximal (eraseLast s).last (last s)

Tactic:
have : s.length - 1 + 1 = s.length := by
  conv_rhs => rw [← Nat.add_one_sub_one s.length]; rw [Nat.succ_sub h]

Result:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
this : s.length - 1 + 1 = s.length
⊢ IsMaximal (eraseLast s).last (last s)

Proof state:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
this : s.length - 1 + 1 = s.length
⊢ IsMaximal (eraseLast s).last (last s)

Tactic:
rw [last_eraseLast, last]

Result:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
this : s.length - 1 + 1 = s.length
⊢ IsMaximal (s.toFun ⟨s.length.pred, ⋯⟩) (s.toFun (Fin.last s.length))

Proof state:
case h.e'_5.h.e'_4.h
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
this : s.length - 1 + 1 = s.length
⊢ ↑(Fin.last s.length) = ↑⟨s.length - 1, ⋯⟩.succ

Tactic:
simp [this]

Result:
no goals

Proof state:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
this : s.length - 1 + 1 = s.length
⊢ s.length - 1 < s.length

Tactic:
omega

Result:
no goals

Proof state:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
⊢ s.length - 1 + 1 = s.length

Tactic:
conv_rhs => rw [← Nat.add_one_sub_one s.length]; rw [Nat.succ_sub h]

Result:
no goals
-- Mathlib/Data/Nat/Factors.lean
theorem perm_primeFactorsList_mul_of_coprime {a b : ℕ} (hab : Coprime a b) :
    (a * b).primeFactorsList ~ a.primeFactorsList ++ b.primeFactorsList

Proof state:
a b : ℕ
hab : a.Coprime b
⊢ (a * b).primeFactorsList ~ a.primeFactorsList ++ b.primeFactorsList

Tactic:
rcases a.eq_zero_or_pos with (rfl | ha)

Result:
case inl
b : ℕ
hab : Coprime 0 b
⊢ (0 * b).primeFactorsList ~ primeFactorsList 0 ++ b.primeFactorsList

case inr
a b : ℕ
hab : a.Coprime b
ha : a > 0
⊢ (a * b).primeFactorsList ~ a.primeFactorsList ++ b.primeFactorsList

Proof state:
case inr.inr
a b : ℕ
hab : a.Coprime b
ha : a > 0
hb : b > 0
⊢ (a * b).primeFactorsList ~ a.primeFactorsList ++ b.primeFactorsList

Tactic:
exact perm_primeFactorsList_mul ha.ne' hb.ne'

Result:
no goals

Proof state:
case inr
a b : ℕ
hab : a.Coprime b
ha : a > 0
⊢ (a * b).primeFactorsList ~ a.primeFactorsList ++ b.primeFactorsList

Tactic:
rcases b.eq_zero_or_pos with (rfl | hb)

Result:
case inr.inl
a : ℕ
ha : a > 0
hab : a.Coprime 0
⊢ (a * 0).primeFactorsList ~ a.primeFactorsList ++ primeFactorsList 0

case inr.inr
a b : ℕ
hab : a.Coprime b
ha : a > 0
hb : b > 0
⊢ (a * b).primeFactorsList ~ a.primeFactorsList ++ b.primeFactorsList

Proof state:
case inr.inl
a : ℕ
ha : a > 0
hab : a.Coprime 0
⊢ (a * 0).primeFactorsList ~ a.primeFactorsList ++ primeFactorsList 0

Tactic:
simp [(coprime_zero_right _).mp hab]

Result:
no goals

Proof state:
case inl
b : ℕ
hab : Coprime 0 b
⊢ (0 * b).primeFactorsList ~ primeFactorsList 0 ++ b.primeFactorsList

Tactic:
simp [(coprime_zero_left _).mp hab]

Result:
no goals
-- Mathlib/FieldTheory/SplittingField/IsSplittingField.lean
theorem of_algEquiv [Algebra K F] (p : K[X]) (f : F ≃ₐ[K] L) [IsSplittingField K F p] :
    IsSplittingField K L p

Proof state:
F : Type u
K : Type v
L : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field F
inst✝² : Algebra K L
inst✝¹ : Algebra K F
p : K[X]
f : F ≃ₐ[K] L
inst✝ : IsSplittingField K F p
⊢ IsSplittingField K L p

Tactic:
constructor

Result:
case splits'
F : Type u
K : Type v
L : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field F
inst✝² : Algebra K L
inst✝¹ : Algebra K F
p : K[X]
f : F ≃ₐ[K] L
inst✝ : IsSplittingField K F p
⊢ Splits (algebraMap K L) p

case adjoin_rootSet'
F : Type u
K : Type v
L : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field F
inst✝² : Algebra K L
inst✝¹ : Algebra K F
p : K[X]
f : F ≃ₐ[K] L
inst✝ : IsSplittingField K F p
⊢ Algebra.adjoin K (p.rootSet L) = ⊤

Proof state:
case splits'
F : Type u
K : Type v
L : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field F
inst✝² : Algebra K L
inst✝¹ : Algebra K F
p : K[X]
f : F ≃ₐ[K] L
inst✝ : IsSplittingField K F p
⊢ Splits ((↑↑f).comp (algebraMap K F)) p

Tactic:
exact splits_comp_of_splits _ _ (splits F p)

Result:
no goals

Proof state:
case splits'
F : Type u
K : Type v
L : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field F
inst✝² : Algebra K L
inst✝¹ : Algebra K F
p : K[X]
f : F ≃ₐ[K] L
inst✝ : IsSplittingField K F p
⊢ Splits (algebraMap K L) p

Tactic:
rw [← f.toAlgHom.comp_algebraMap]

Result:
case splits'
F : Type u
K : Type v
L : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field F
inst✝² : Algebra K L
inst✝¹ : Algebra K F
p : K[X]
f : F ≃ₐ[K] L
inst✝ : IsSplittingField K F p
⊢ Splits ((↑↑f).comp (algebraMap K F)) p

Proof state:
case adjoin_rootSet'
F : Type u
K : Type v
L : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field F
inst✝² : Algebra K L
inst✝¹ : Algebra K F
p : K[X]
f : F ≃ₐ[K] L
inst✝ : IsSplittingField K F p
⊢ Algebra.adjoin K (p.rootSet L) = ⊤

Tactic:
rw [← (AlgHom.range_eq_top f.toAlgHom).mpr f.surjective,
  adjoin_rootSet_eq_range (splits F p), adjoin_rootSet F p]

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
lemma H1π_eq_zero_iff (x : oneCocycles A) : H1π A x = 0 ↔ ⇑x ∈ oneCoboundaries A

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(oneCocycles A)
⊢ (LinearMap.range (LinearMap.codRestrict (oneCocycles A) (dZero A) ⋯)).mkQ x = 0 ↔ ⇑x ∈ oneCoboundaries A

Tactic:
simp [LinearMap.range_codRestrict, oneCoboundaries]

Result:
no goals

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(oneCocycles A)
⊢ (ConcreteCategory.hom (H1π A)) x = 0 ↔ ⇑x ∈ oneCoboundaries A

Tactic:
show (LinearMap.range ((dZero A).codRestrict (oneCocycles A) _)).mkQ _ = 0 ↔ _

Result:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(oneCocycles A)
⊢ (LinearMap.range (LinearMap.codRestrict (oneCocycles A) (dZero A) ⋯)).mkQ x = 0 ↔ ⇑x ∈ oneCoboundaries A
-- Mathlib/Algebra/Group/Submonoid/Finsupp.lean
theorem mem_closure_range_iff_of_fintype [Fintype ι] :
    x ∈ closure (Set.range f) ↔ ∃ a : ι → ℕ, x = ∏ i, f i ^ a i

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
inst✝ : Fintype ι
⊢ (∃ a, x = a.prod fun x1 x2 => f x1 ^ x2) ↔ ∃ b, x = ∏ i : ι, f i ^ Finsupp.equivFunOnFinite.symm.symm b i

Tactic:
simp

Result:
no goals

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
inst✝ : Fintype ι
⊢ x ∈ closure (Set.range f) ↔ ∃ a, x = ∏ i : ι, f i ^ a i

Tactic:
rw [Finsupp.equivFunOnFinite.symm.exists_congr_left, mem_closure_range_iff]

Result:
M : Type u_1
inst✝¹ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
inst✝ : Fintype ι
⊢ (∃ a, x = a.prod fun x1 x2 => f x1 ^ x2) ↔ ∃ b, x = ∏ i : ι, f i ^ Finsupp.equivFunOnFinite.symm.symm b i
-- Mathlib/Data/Matrix/PEquiv.lean
theorem toMatrix_swap [DecidableEq n] [Ring α] (i j : n) :
    (Equiv.swap i j).toPEquiv.toMatrix =
      (1 : Matrix n n α) - (single i i).toMatrix - (single j j).toMatrix + (single i j).toMatrix +
        (single j i).toMatrix

Proof state:
case a
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ j✝ : n
⊢ (if j✝ ∈ some (if i✝ = i then j else if i✝ = j then i else i✝) then 1 else 0) =
    ((((if i✝ = j✝ then 1 else 0) - if j✝ ∈ if i✝ = i then some i else none then 1 else 0) -
          if j✝ ∈ if i✝ = j then some j else none then 1 else 0) +
        if j✝ ∈ if i✝ = i then some j else none then 1 else 0) +
      if j✝ ∈ if i✝ = j then some i else none then 1 else 0

Tactic:
split_ifs <;> simp_all

Result:
no goals

Proof state:
case a
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ j✝ : n
⊢ (Equiv.toPEquiv (Equiv.swap i j)).toMatrix i✝ j✝ =
    (1 - (single i i).toMatrix - (single j j).toMatrix + (single i j).toMatrix + (single j i).toMatrix) i✝ j✝

Tactic:
dsimp [toMatrix, single, Equiv.swap_apply_def, Equiv.toPEquiv, one_apply]

Result:
case a
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ j✝ : n
⊢ (if j✝ ∈ some (if i✝ = i then j else if i✝ = j then i else i✝) then 1 else 0) =
    ((((if i✝ = j✝ then 1 else 0) - if j✝ ∈ if i✝ = i then some i else none then 1 else 0) -
          if j✝ ∈ if i✝ = j then some j else none then 1 else 0) +
        if j✝ ∈ if i✝ = i then some j else none then 1 else 0) +
      if j✝ ∈ if i✝ = j then some i else none then 1 else 0

Proof state:
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j : n
⊢ (Equiv.toPEquiv (Equiv.swap i j)).toMatrix =
    1 - (single i i).toMatrix - (single j j).toMatrix + (single i j).toMatrix + (single j i).toMatrix

Tactic:
ext

Result:
case a
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ j✝ : n
⊢ (Equiv.toPEquiv (Equiv.swap i j)).toMatrix i✝ j✝ =
    (1 - (single i i).toMatrix - (single j j).toMatrix + (single i j).toMatrix + (single j i).toMatrix) i✝ j✝
-- Mathlib/Topology/Algebra/ProperAction/Basic.lean
theorem properSMul_iff_continuousSMul_ultrafilter_tendsto :
    ProperSMul G X ↔ ContinuousSMul G X ∧
      (∀ 𝒰 : Ultrafilter (G × X), ∀ x₁ x₂ : X,
        Tendsto (fun gx : G × X ↦ (gx.1 • gx.2, gx.2)) 𝒰 (𝓝 (x₁, x₂)) →
      ∃ g : G, g • x₂ = x₁ ∧ Tendsto (Prod.fst : G × X → G) 𝒰 (𝓝 g))

Proof state:
case refine_1
G : Type u_1
X : Type u_2
inst✝³ : Group G
inst✝² : MulAction G X
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalSpace X
h :
  (Continuous fun gx => (gx.1 • gx.2, gx.2)) ∧
    ∀ ⦃𝒰 : Ultrafilter (G × X)⦄ ⦃y : X × X⦄,
      Tendsto (fun gx => (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 y) → ∃ x, (x.1 • x.2, x.2) = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter (G × X)
x₁ x₂ : X
h' : Tendsto (fun gx => (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂))
⊢ ∃ g, g • x₂ = x₁ ∧ Tendsto fst (↑𝒰) (𝓝 g)

Tactic:
rcases h.2 h' with ⟨gx, hgx1, hgx2⟩

Result:
case refine_1.intro.intro
G : Type u_1
X : Type u_2
inst✝³ : Group G
inst✝² : MulAction G X
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalSpace X
h :
  (Continuous fun gx => (gx.1 • gx.2, gx.2)) ∧
    ∀ ⦃𝒰 : Ultrafilter (G × X)⦄ ⦃y : X × X⦄,
      Tendsto (fun gx => (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 y) → ∃ x, (x.1 • x.2, x.2) = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter (G × X)
x₁ x₂ : X
h' : Tendsto (fun gx => (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂))
gx : G × X
hgx1 : (gx.1 • gx.2, gx.2) = (x₁, x₂)
hgx2 : ↑𝒰 ≤ 𝓝 gx
⊢ ∃ g, g • x₂ = x₁ ∧ Tendsto fst (↑𝒰) (𝓝 g)

Proof state:
case refine_1.intro.intro
G : Type u_1
X : Type u_2
inst✝³ : Group G
inst✝² : MulAction G X
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalSpace X
h :
  (Continuous fun gx => (gx.1 • gx.2, gx.2)) ∧
    ∀ ⦃𝒰 : Ultrafilter (G × X)⦄ ⦃y : X × X⦄,
      Tendsto (fun gx => (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 y) → ∃ x, (x.1 • x.2, x.2) = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter (G × X)
x₁ x₂ : X
h' : Tendsto (fun gx => (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂))
gx : G × X
hgx2 : ↑𝒰 ≤ 𝓝 gx
hgx1 : gx.1 • gx.2 = x₁ ∧ gx.2 = x₂
⊢ gx.1 • x₂ = x₁

Tactic:
rw [← hgx1.2, hgx1.1]

Result:
no goals
-- Mathlib/ModelTheory/Syntax.lean
theorem relabel_id (t : L.Term α) : t.relabel id = t

Proof state:
case var
L : Language
α : Type u'
a✝ : α
⊢ relabel id (var a✝) = var a✝

Tactic:
rfl

Result:
no goals

Proof state:
L : Language
α : Type u'
t : L.Term α
⊢ relabel id t = t

Tactic:
induction t with
| var => rfl
| func _ _ ih => simp [ih]

Result:
no goals

Proof state:
case func
L : Language
α : Type u'
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
ih : ∀ (a : Fin l✝), relabel id (_ts✝ a) = _ts✝ a
⊢ relabel id (func _f✝ _ts✝) = func _f✝ _ts✝

Tactic:
simp [ih]

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Monoidal/Normalize.lean
theorem evalWhiskerLeft_id {f g : C} {η : f ⟶ g}
    {η₁ : f ⟶ 𝟙_ C ⊗ g} {η₂ : 𝟙_ C ⊗ f ⟶ 𝟙_ C ⊗ g}
    (e_η₁ : η ≫ (λ_ _).inv = η₁) (e_η₂ : (λ_ _).hom ≫ η₁ = η₂) :
    𝟙_ C ◁ η = η₂

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g : C
η : f ⟶ g
η₁ : f ⟶ 𝟙_ C ⊗ g
η₂ : 𝟙_ C ⊗ f ⟶ 𝟙_ C ⊗ g
e_η₁ : η ≫ (λ_ g).inv = η₁
e_η₂ : (λ_ f).hom ≫ η₁ = η₂
⊢ 𝟙_ C ◁ η = η₂

Tactic:
simp [e_η₁, e_η₂]

Result:
no goals