harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean
lemma isIso_π (hf : S.f = 0) : IsIso h.π

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.LeftHomologyData
hf : S.f = 0
⊢ h.f' ≫ 𝟙 h.K = 0

Tactic:
rw [← cancel_mono h.i, comp_id, f'_i, zero_comp, hf]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.LeftHomologyData
hf : S.f = 0
φ : (CokernelCofork.ofπ h.π ⋯).pt ⟶ h.K
hφ : h.π ≫ φ = 𝟙 h.K
⊢ φ ≫ h.π = 𝟙 h.H

Tactic:
rw [← cancel_epi h.π, reassoc_of% hφ, comp_id]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.LeftHomologyData
hf : S.f = 0
φ : (CokernelCofork.ofπ h.π ⋯).pt ⟶ h.K
hφ : h.π ≫ φ = 𝟙 h.K
⊢ IsIso h.π

Tactic:
exact ⟨φ, hφ, by rw [← cancel_epi h.π, reassoc_of% hφ, comp_id]⟩

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.LeftHomologyData
hf : S.f = 0
φ : (CokernelCofork.ofπ h.π ⋯).pt ⟶ h.K
hφ : Cofork.π (CokernelCofork.ofπ h.π ⋯) ≫ φ = 𝟙 h.K
⊢ IsIso h.π

Tactic:
dsimp at hφ

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.LeftHomologyData
hf : S.f = 0
φ : (CokernelCofork.ofπ h.π ⋯).pt ⟶ h.K
hφ : h.π ≫ φ = 𝟙 h.K
⊢ IsIso h.π

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.LeftHomologyData
hf : S.f = 0
⊢ IsIso h.π

Tactic:
have ⟨φ, hφ⟩ := CokernelCofork.IsColimit.desc' h.hπ' (𝟙 _)
  (by rw [← cancel_mono h.i, comp_id, f'_i, zero_comp, hf])

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.LeftHomologyData
hf : S.f = 0
φ : (CokernelCofork.ofπ h.π ⋯).pt ⟶ h.K
hφ : Cofork.π (CokernelCofork.ofπ h.π ⋯) ≫ φ = 𝟙 h.K
⊢ IsIso h.π
-- Mathlib/Algebra/Quaternion.lean
theorem coe_mul : ((x * y : R) : ℍ[R,c₁,c₂,c₃]) = x * y

Proof state:
R : Type u_3
c₁ c₂ c₃ x y : R
inst✝ : CommRing R
⊢ ↑(x * y) = ↑x * ↑y

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Order/Closure.lean
theorem setOf_isClosed_eq_range_closure : {x | c.IsClosed x} = Set.range c

Proof state:
case h
α : Type u_1
inst✝ : PartialOrder α
c : ClosureOperator α
x : α
⊢ x ∈ {x | c.IsClosed x} ↔ x ∈ range ⇑c

Tactic:
exact ⟨fun hx ↦ ⟨x, hx.closure_eq⟩, by rintro ⟨y, rfl⟩; exact c.isClosed_closure _⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : PartialOrder α
c : ClosureOperator α
⊢ {x | c.IsClosed x} = range ⇑c

Tactic:
ext x

Result:
case h
α : Type u_1
inst✝ : PartialOrder α
c : ClosureOperator α
x : α
⊢ x ∈ {x | c.IsClosed x} ↔ x ∈ range ⇑c

Proof state:
case intro
α : Type u_1
inst✝ : PartialOrder α
c : ClosureOperator α
y : α
⊢ c y ∈ {x | c.IsClosed x}

Tactic:
exact c.isClosed_closure _

Result:
no goals

Proof state:
α : Type u_1
inst✝ : PartialOrder α
c : ClosureOperator α
x : α
⊢ x ∈ range ⇑c → x ∈ {x | c.IsClosed x}

Tactic:
rintro ⟨y, rfl⟩

Result:
case intro
α : Type u_1
inst✝ : PartialOrder α
c : ClosureOperator α
y : α
⊢ c y ∈ {x | c.IsClosed x}
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem isLittleO_const_left {c : E''} :
    (fun _x => c) =o[l] g'' ↔ c = 0 ∨ Tendsto (norm ∘ g'') l atTop

Proof state:
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
g'' : α → F''
l : Filter α
c : E''
⊢ (fun _x => c) =o[l] g'' ↔ c = 0 ∨ Tendsto (norm ∘ g'') l atTop

Tactic:
rcases eq_or_ne c 0 with (rfl | hc)

Result:
case inl
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
g'' : α → F''
l : Filter α
⊢ (fun _x => 0) =o[l] g'' ↔ 0 = 0 ∨ Tendsto (norm ∘ g'') l atTop

case inr
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
g'' : α → F''
l : Filter α
c : E''
hc : c ≠ 0
⊢ (fun _x => c) =o[l] g'' ↔ c = 0 ∨ Tendsto (norm ∘ g'') l atTop

Proof state:
case inl
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
g'' : α → F''
l : Filter α
⊢ (fun _x => 0) =o[l] g'' ↔ 0 = 0 ∨ Tendsto (norm ∘ g'') l atTop

Tactic:
simp only [isLittleO_zero, eq_self_iff_true, true_or]

Result:
no goals

Proof state:
case inr
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
g'' : α → F''
l : Filter α
c : E''
hc : c ≠ 0
⊢ Tendsto (fun x => ‖g'' x‖) l atTop ↔ Tendsto (norm ∘ g'') l atTop

Tactic:
rfl

Result:
no goals

Proof state:
case inr
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
g'' : α → F''
l : Filter α
c : E''
hc : c ≠ 0
⊢ (fun _x => c) =o[l] g'' ↔ c = 0 ∨ Tendsto (norm ∘ g'') l atTop

Tactic:
simp only [hc, false_or, isLittleO_const_left_of_ne hc]

Result:
case inr
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
g'' : α → F''
l : Filter α
c : E''
hc : c ≠ 0
⊢ Tendsto (fun x => ‖g'' x‖) l atTop ↔ Tendsto (norm ∘ g'') l atTop
-- Mathlib/Topology/CompactOpen.lean
theorem nhds_compactOpen_eq_iInf_nhds_induced (f : C(X, Y)) :
    𝓝 f = ⨅ (s) (_ : IsCompact s), (𝓝 (f.restrict s)).comap (ContinuousMap.restrict s)

Proof state:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
⊢ 𝓝 f = ⨅ s, ⨅ (_ : IsCompact s), comap (restrict s) (𝓝 (restrict s f))

Tactic:
simp only [nhds_iInf, nhds_induced]

Result:
no goals
-- Mathlib/Algebra/Lie/Derivation/Killing.lean
lemma ad_mem_ker_killingForm_ad_range_of_mem_orthogonal
    {D : LieDerivation R L L} (hD : D ∈ 𝕀ᗮ) (x : L) :
    ad R L (D x) ∈ (LinearMap.ker (killingForm R 𝕀)).map (LieHom.range (ad R L)).subtype

Proof state:
R : Type u_1
L : Type u_2
inst✝³ : Field R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : Module.Finite R L
D : LieDerivation R L L
hD : D ∈ (killingForm R (LieDerivation R L L)).orthogonal (ad R L).range.toSubmodule
x : L
⊢ (ad R L) (D x) ∈ Submodule.map (ad R L).range.subtype (LinearMap.ker (killingForm R ↥(ad R L).range))

Tactic:
rw [← killingForm_restrict_range_ad]

Result:
R : Type u_1
L : Type u_2
inst✝³ : Field R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : Module.Finite R L
D : LieDerivation R L L
hD : D ∈ (killingForm R (LieDerivation R L L)).orthogonal (ad R L).range.toSubmodule
x : L
⊢ (ad R L) (D x) ∈
    Submodule.map (ad R L).range.subtype
      (LinearMap.ker ((killingForm R (LieDerivation R L L)).restrict (ad R L).range.toSubmodule))

Proof state:
R : Type u_1
L : Type u_2
inst✝³ : Field R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : Module.Finite R L
D : LieDerivation R L L
hD : D ∈ (killingForm R (LieDerivation R L L)).orthogonal (ad R L).range.toSubmodule
x : L
⊢ (ad R L) (D x) ∈
    Submodule.map (ad R L).range.subtype
      (LinearMap.ker ((killingForm R (LieDerivation R L L)).restrict (ad R L).range.toSubmodule))

Tactic:
exact LinearMap.BilinForm.inf_orthogonal_self_le_ker_restrict
  (LieModule.traceForm_isSymm R 𝔻 𝔻).isRefl ⟨by simp, ad_mem_orthogonal_of_mem_orthogonal hD x⟩

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
inst✝³ : Field R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : Module.Finite R L
D : LieDerivation R L L
hD : D ∈ (killingForm R (LieDerivation R L L)).orthogonal (ad R L).range.toSubmodule
x : L
⊢ (ad R L) (D x) ∈ ↑(ad R L).range.toSubmodule

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Diagonal.lean
theorem diagonalObjPullbackFstIso_inv_snd_fst {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) :
    (diagonalObjPullbackFstIso f g).inv ≫ pullback.snd _ _ ≫ pullback.fst _ _ =
      pullback.snd _ _

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (diagonalObjPullbackFstIso f g).inv ≫ snd (fst f g) (fst f g) ≫ fst f g = snd (snd g g ≫ g) f

Tactic:
delta diagonalObjPullbackFstIso

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullbackRightPullbackFstIso f g (fst f g) ≪≫
          congrHom ⋯ ⋯ ≪≫ pullbackAssoc f g g g ≪≫ pullbackSymmetry f (fst g g ≫ g) ≪≫ congrHom ⋯ ⋯).inv ≫
      snd (fst f g) (fst f g) ≫ fst f g =
    snd (snd g g ≫ g) f

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullbackRightPullbackFstIso f g (fst f g) ≪≫
          congrHom ⋯ ⋯ ≪≫ pullbackAssoc f g g g ≪≫ pullbackSymmetry f (fst g g ≫ g) ≪≫ congrHom ⋯ ⋯).inv ≫
      snd (fst f g) (fst f g) ≫ fst f g =
    snd (snd g g ≫ g) f

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Real/Sqrt.lean
lemma sqrt_le_sqrt_iff' (hx : 0 < x) : √x ≤ √y ↔ x ≤ y

Proof state:
case inl
x y : ℝ
hx : 0 < x
hy : y ≤ 0
⊢ √x ≤ √y ↔ x ≤ y

Tactic:
exact iff_of_false ((sqrt_eq_zero_of_nonpos hy).trans_lt <| sqrt_pos.2 hx).not_le
  (hy.trans_lt hx).not_le

Result:
no goals

Proof state:
case inr
x y : ℝ
hx : 0 < x
hy : 0 ≤ y
⊢ √x ≤ √y ↔ x ≤ y

Tactic:
exact sqrt_le_sqrt_iff hy

Result:
no goals

Proof state:
x y : ℝ
hx : 0 < x
⊢ √x ≤ √y ↔ x ≤ y

Tactic:
obtain hy | hy := le_total y 0

Result:
case inl
x y : ℝ
hx : 0 < x
hy : y ≤ 0
⊢ √x ≤ √y ↔ x ≤ y

case inr
x y : ℝ
hx : 0 < x
hy : 0 ≤ y
⊢ √x ≤ √y ↔ x ≤ y
-- Mathlib/LinearAlgebra/ExteriorPower/Basic.lean
@[simp]
lemma map_apply_ιMulti_family {I : Type*} [LinearOrder I] (v : I → M) (f : M →ₗ[R] N)
  (s : {s : Finset I // s.card = n}) :
    (map n f) (ιMulti_family R n v s) = ιMulti_family R n (f ∘ v) s

Proof state:
R : Type u
inst✝⁵ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
I : Type u_4
inst✝ : LinearOrder I
v : I → M
f : M →ₗ[R] N
s : { s // s.card = n }
⊢ (map n f) (ιMulti_family R n v s) = ιMulti_family R n (⇑f ∘ v) s

Tactic:
simp only [ιMulti_family, map, alternatingMapLinearEquiv_apply_ιMulti]

Result:
R : Type u
inst✝⁵ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
I : Type u_4
inst✝ : LinearOrder I
v : I → M
f : M →ₗ[R] N
s : { s // s.card = n }
⊢ (((ιMulti R n).compLinearMap f) fun i => v ↑(((↑s).orderIsoOfFin ⋯) i)) =
    (ιMulti R n) fun i => (⇑f ∘ v) ↑(((↑s).orderIsoOfFin ⋯) i)

Proof state:
R : Type u
inst✝⁵ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
I : Type u_4
inst✝ : LinearOrder I
v : I → M
f : M →ₗ[R] N
s : { s // s.card = n }
⊢ (((ιMulti R n).compLinearMap f) fun i => v ↑(((↑s).orderIsoOfFin ⋯) i)) =
    (ιMulti R n) fun i => (⇑f ∘ v) ↑(((↑s).orderIsoOfFin ⋯) i)

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/List/DropRight.lean
theorem rdropWhile_last_not (hl : l.rdropWhile p ≠ []) : ¬p ((rdropWhile p l).getLast hl)

Proof state:
α : Type u_1
p : α → Bool
l : List α
hl : rdropWhile p l ≠ []
⊢ ¬p ((rdropWhile p l).getLast hl) = true

Tactic:
simp_rw [rdropWhile]

Result:
α : Type u_1
p : α → Bool
l : List α
hl : rdropWhile p l ≠ []
⊢ ¬p ((dropWhile p l.reverse).reverse.getLast ⋯) = true

Proof state:
α : Type u_1
p : α → Bool
l : List α
hl : rdropWhile p l ≠ []
⊢ ¬p ((dropWhile p l.reverse).reverse.getLast ⋯) = true

Tactic:
rw [getLast_reverse, head_dropWhile_not p]

Result:
α : Type u_1
p : α → Bool
l : List α
hl : rdropWhile p l ≠ []
⊢ ¬false = true

Proof state:
α : Type u_1
p : α → Bool
l : List α
hl : rdropWhile p l ≠ []
⊢ ¬false = true

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Analytic/Composition.lean
theorem AnalyticAt.comp_analyticWithinAt_of_eq {g : F → G} {f : E → F} {x : E} {y : F} {s : Set E}
    (hg : AnalyticAt 𝕜 g y) (hf : AnalyticWithinAt 𝕜 f s x) (h : f x = y) :
    AnalyticWithinAt 𝕜 (g ∘ f) s x

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : F → G
f : E → F
x : E
y : F
s : Set E
hg : AnalyticAt 𝕜 g (f x)
hf : AnalyticWithinAt 𝕜 f s x
h : f x = y
⊢ AnalyticWithinAt 𝕜 (g ∘ f) s x

Tactic:
exact hg.comp_analyticWithinAt hf

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : F → G
f : E → F
x : E
y : F
s : Set E
hg : AnalyticAt 𝕜 g y
hf : AnalyticWithinAt 𝕜 f s x
h : f x = y
⊢ AnalyticWithinAt 𝕜 (g ∘ f) s x

Tactic:
rw [← h] at hg

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : F → G
f : E → F
x : E
y : F
s : Set E
hg : AnalyticAt 𝕜 g (f x)
hf : AnalyticWithinAt 𝕜 f s x
h : f x = y
⊢ AnalyticWithinAt 𝕜 (g ∘ f) s x
-- Mathlib/CategoryTheory/Limits/Shapes/StrongEpi.lean
theorem strongEpi_comp [StrongEpi f] [StrongEpi g] : StrongEpi (f ≫ g) :=
  { epi := epi_comp _ _
    llp

Proof state:
C : Type u
inst✝² : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝¹ : StrongEpi f
inst✝ : StrongEpi g
⊢ ∀ ⦃X Y : C⦄ (z : X ⟶ Y) [inst : Mono z], HasLiftingProperty (f ≫ g) z

Tactic:
intros

Result:
C : Type u
inst✝³ : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝² : StrongEpi f
inst✝¹ : StrongEpi g
X✝ Y✝ : C
z✝ : X✝ ⟶ Y✝
inst✝ : Mono z✝
⊢ HasLiftingProperty (f ≫ g) z✝

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝² : StrongEpi f
inst✝¹ : StrongEpi g
X✝ Y✝ : C
z✝ : X✝ ⟶ Y✝
inst✝ : Mono z✝
⊢ HasLiftingProperty (f ≫ g) z✝

Tactic:
infer_instance

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem?_eq_some_iff {a : Array α} : a[i]? = some b ↔ ∃ h : i < a.size, a[i] = b

Proof state:
α : Type u_1
i : Nat
b : α
a : Array α
⊢ a[i]? = some b ↔ ∃ h, a[i] = b

Tactic:
simp [getElem?_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem not_not {b : BitVec w} : ~~~(~~~b) = b

Proof state:
w : Nat
b : BitVec w
⊢ ~~~~~~b = b

Tactic:
ext i h

Result:
case pred
w : Nat
b : BitVec w
i : Nat
h : i < w
⊢ (~~~~~~b).getLsbD i = b.getLsbD i

Proof state:
case pred
w : Nat
b : BitVec w
i : Nat
h : i < w
⊢ (~~~~~~b).getLsbD i = b.getLsbD i

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem image_const_sub_Ici : (fun x => a - x) '' Ici b = Iic (a - b)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b : α
this : ∀ (a_1 : Set α), (fun x => a + -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Ici b = Iic (a - b)

Tactic:
simp [sub_eq_add_neg, this, add_comm]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b : α
this : ∀ (a_1 : Set α), ((fun x => a + x) ∘ fun x => -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Ici b = Iic (a - b)

Tactic:
dsimp [Function.comp_def] at this

Result:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b : α
this : ∀ (a_1 : Set α), (fun x => a + -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Ici b = Iic (a - b)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b : α
⊢ (fun x => a - x) '' Ici b = Iic (a - b)

Tactic:
have := image_comp (fun x => a + x) fun x => -x

Result:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b : α
this : ∀ (a_1 : Set α), ((fun x => a + x) ∘ fun x => -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Ici b = Iic (a - b)
-- Mathlib/CategoryTheory/Limits/HasLimits.lean
theorem colimit.desc_extend (F : J ⥤ C) [HasColimit F] (c : Cocone F) {X : C} (f : c.pt ⟶ X) :
    colimit.desc F (c.extend f) = colimit.desc F c ≫ f

Proof state:
case w
J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasColimit F
c : Cocone F
X : C
f : c.pt ⟶ X
j✝ : J
⊢ ι F j✝ ≫ desc F (c.extend f) = (ι F j✝ ≫ desc F c) ≫ f

Tactic:
simp

Result:
no goals

Proof state:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasColimit F
c : Cocone F
X : C
f : c.pt ⟶ X
⊢ desc F (c.extend f) = desc F c ≫ f

Tactic:
ext1

Result:
case w
J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasColimit F
c : Cocone F
X : C
f : c.pt ⟶ X
j✝ : J
⊢ ι F j✝ ≫ desc F (c.extend f) = ι F j✝ ≫ desc F c ≫ f

Proof state:
case w
J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasColimit F
c : Cocone F
X : C
f : c.pt ⟶ X
j✝ : J
⊢ ι F j✝ ≫ desc F (c.extend f) = ι F j✝ ≫ desc F c ≫ f

Tactic:
rw [← Category.assoc]

Result:
case w
J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasColimit F
c : Cocone F
X : C
f : c.pt ⟶ X
j✝ : J
⊢ ι F j✝ ≫ desc F (c.extend f) = (ι F j✝ ≫ desc F c) ≫ f
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem enum_eq_cons_iff {l : List α} :
    l.enum = x :: l' ↔ ∃ a as, l = a :: as ∧ x = (0, a) ∧ l' = enumFrom 1 as

Proof state:
α : Type u_1
x : Nat × α
l' : List (Nat × α)
l : List α
⊢ l.enum = x :: l' ↔ ∃ a as, l = a :: as ∧ x = (0, a) ∧ l' = enumFrom 1 as

Tactic:
rw [enum, enumFrom_eq_cons_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem get!_ofList_of_mem [LawfulBEq α]
    {l : List ((a : α) × β a)} {k k' : α} (k_beq : k == k') {v : β k} [Inhabited (β k')]
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : ⟨k, v⟩ ∈ l) :
    (ofList l).get! k' = cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v :=
  Raw₀.get!_insertMany_empty_list_of_mem k_beq distinct mem

Proof state:
case e_a
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
inst✝¹ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
inst✝ : Inhabited (β k')
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ k = k'

Tactic:
apply LawfulBEq.eq_of_beq k_beq

Result:
no goals

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
inst✝¹ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
inst✝ : Inhabited (β k')
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ β k = β k'

Tactic:
congr

Result:
case e_a
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
inst✝¹ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
inst✝ : Inhabited (β k')
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ k = k'
-- Mathlib/Data/Option/Basic.lean
@[simp]
lemma bnot_comp_isSome : (! ·) ∘ @Option.isSome α = Option.isNone

Proof state:
case h
α : Type u_1
x✝ : Option α
⊢ ((fun x => !x) ∘ isSome) x✝ = x✝.isNone

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
⊢ (fun x => !x) ∘ isSome = isNone

Tactic:
funext

Result:
case h
α : Type u_1
x✝ : Option α
⊢ ((fun x => !x) ∘ isSome) x✝ = x✝.isNone
-- Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean
theorem IsIntegral.det {n : Type*} [Fintype n] [DecidableEq n] {M : Matrix n n A}
    (h : ∀ i j, IsIntegral R (M i j)) : IsIntegral R M.det

Proof state:
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
n : Type u_5
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n A
h : ∀ (i j : n), IsIntegral R (M i j)
⊢ IsIntegral R M.det

Tactic:
rw [Matrix.det_apply]

Result:
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
n : Type u_5
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n A
h : ∀ (i j : n), IsIntegral R (M i j)
⊢ IsIntegral R (∑ σ : Equiv.Perm n, Equiv.Perm.sign σ • ∏ i : n, M (σ i) i)

Proof state:
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
n : Type u_5
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n A
h : ∀ (i j : n), IsIntegral R (M i j)
⊢ IsIntegral R (∑ σ : Equiv.Perm n, Equiv.Perm.sign σ • ∏ i : n, M (σ i) i)

Tactic:
exact IsIntegral.sum _ fun σ _hσ ↦ (IsIntegral.prod _ fun i _hi => h _ _).zsmul _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem mapIdx_eq_cons_iff' {l : List α} {b : β} :
    mapIdx f l = b :: l₂ ↔
      l.head?.map (f 0) = some b ∧ l.tail?.map (mapIdx fun i => f (i + 1)) = some l₂

Proof state:
α : Type u_1
β : Type u_2
f : Nat → α → β
l₂ : List β
l : List α
b : β
⊢ mapIdx f l = b :: l₂ ↔ Option.map (f 0) l.head? = some b ∧ Option.map (mapIdx fun i => f (i + 1)) l.tail? = some l₂

Tactic:
cases l <;> simp

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma add_ne_top_iff_ne_top₂ {x y : EReal} (hx : x ≠ ⊥) (hy : y ≠ ⊥) :
    x + y ≠ ⊤ ↔ x ≠ ⊤ ∧ y ≠ ⊤

Proof state:
x y : EReal
hx : x ≠ ⊥
hy : y ≠ ⊥
⊢ x + y ≠ ⊤ ↔ x ≠ ⊤ ∧ y ≠ ⊤

Tactic:
refine ⟨?_, fun h ↦ add_ne_top h.1 h.2⟩

Result:
x y : EReal
hx : x ≠ ⊥
hy : y ≠ ⊥
⊢ x + y ≠ ⊤ → x ≠ ⊤ ∧ y ≠ ⊤

Proof state:
case h_real
y : EReal
a✝ : ℝ
hy : ¬y = ⊥
hx : ¬↑a✝ = ⊥
⊢ ¬↑a✝ + y = ⊤ → ¬↑a✝ = ⊤ ∧ ¬y = ⊤

Tactic:
cases y <;> simp_all only [not_false_eq_true, ne_eq, add_top_of_ne_bot, not_true_eq_false,
  coe_ne_top, and_self, implies_true]

Result:
no goals

Proof state:
x y : EReal
hx : x ≠ ⊥
hy : y ≠ ⊥
⊢ x + y ≠ ⊤ → x ≠ ⊤ ∧ y ≠ ⊤

Tactic:
cases x <;> simp_all only [ne_eq, not_false_eq_true, top_add_of_ne_bot, not_true_eq_false,
  IsEmpty.forall_iff]

Result:
case h_real
y : EReal
a✝ : ℝ
hy : ¬y = ⊥
hx : ¬↑a✝ = ⊥
⊢ ¬↑a✝ + y = ⊤ → ¬↑a✝ = ⊤ ∧ ¬y = ⊤
-- Mathlib/Algebra/Group/Conj.lean
theorem conj_zpow {i : ℤ} {a b : α} : (a * b * a⁻¹) ^ i = a * b ^ i * a⁻¹

Proof state:
α : Type u
inst✝ : Group α
i : ℤ
a b : α
⊢ (a * b * a⁻¹) ^ i = a * b ^ i * a⁻¹

Tactic:
cases i

Result:
case ofNat
α : Type u
inst✝ : Group α
a b : α
a✝ : ℕ
⊢ (a * b * a⁻¹) ^ Int.ofNat a✝ = a * b ^ Int.ofNat a✝ * a⁻¹

case negSucc
α : Type u
inst✝ : Group α
a b : α
a✝ : ℕ
⊢ (a * b * a⁻¹) ^ Int.negSucc a✝ = a * b ^ Int.negSucc a✝ * a⁻¹

Proof state:
case negSucc
α : Type u
inst✝ : Group α
a b : α
a✝ : ℕ
⊢ a * ((b ^ (a✝ + 1))⁻¹ * a⁻¹) = a * (b ^ (a✝ + 1))⁻¹ * a⁻¹

Tactic:
rw [mul_assoc]

Result:
no goals

Proof state:
case negSucc
α : Type u
inst✝ : Group α
a b : α
a✝ : ℕ
⊢ (a * b * a⁻¹) ^ Int.negSucc a✝ = a * b ^ Int.negSucc a✝ * a⁻¹

Tactic:
simp only [zpow_negSucc, conj_pow, mul_inv_rev, inv_inv]

Result:
case negSucc
α : Type u
inst✝ : Group α
a b : α
a✝ : ℕ
⊢ a * ((b ^ (a✝ + 1))⁻¹ * a⁻¹) = a * (b ^ (a✝ + 1))⁻¹ * a⁻¹

Proof state:
case ofNat
α : Type u
inst✝ : Group α
a b : α
a✝ : ℕ
⊢ (a * b * a⁻¹) ^ Int.ofNat a✝ = a * b ^ Int.ofNat a✝ * a⁻¹

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Count.lean
theorem countP_flatMap (p : β → Bool) (l : List α) (f : α → List β) :
    countP p (l.flatMap f) = sum (map (countP p ∘ f) l)

Proof state:
α : Type u_2
β : Type u_1
p : β → Bool
l : List α
f : α → List β
⊢ countP p (flatMap f l) = (map (countP p ∘ f) l).sum

Tactic:
rw [List.flatMap, countP_flatten, map_map]

Result:
no goals
-- Mathlib/Data/Nat/GCD/Basic.lean
theorem coprime_self_add_left {m n : ℕ} : Coprime (m + n) m ↔ Coprime n m

Proof state:
m n : ℕ
⊢ (m + n).Coprime m ↔ n.Coprime m

Tactic:
rw [Coprime, Coprime, gcd_self_add_left]

Result:
no goals