harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem coinduced_continuous {α β : Type*} [t : TopologicalSpace α] [Group β] (f : α → β) :
    Continuous[t, (coinduced f).toTopologicalSpace] f

Proof state:
α : Type u_1
β : Type u_2
t : TopologicalSpace α
inst✝ : Group β
f : α → β
⊢ ∀ t_1 ∈ toTopologicalSpace '' {b | TopologicalSpace.coinduced f t ≤ b.toTopologicalSpace}, Continuous f

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

Result:
case intro.intro
α : Type u_1
β : Type u_2
t : TopologicalSpace α
inst✝ : Group β
f : α → β
t' : GroupTopology β
ht' : t' ∈ {b | TopologicalSpace.coinduced f t ≤ b.toTopologicalSpace}
⊢ Continuous f

Proof state:
α : Type u_1
β : Type u_2
t : TopologicalSpace α
inst✝ : Group β
f : α → β
⊢ Continuous f

Tactic:
rw [continuous_sInf_rng]

Result:
α : Type u_1
β : Type u_2
t : TopologicalSpace α
inst✝ : Group β
f : α → β
⊢ ∀ t_1 ∈ toTopologicalSpace '' {b | TopologicalSpace.coinduced f t ≤ b.toTopologicalSpace}, Continuous f

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
t : TopologicalSpace α
inst✝ : Group β
f : α → β
t' : GroupTopology β
ht' : t' ∈ {b | TopologicalSpace.coinduced f t ≤ b.toTopologicalSpace}
⊢ Continuous f

Tactic:
exact continuous_iff_coinduced_le.2 ht'

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem reverse_range' : ∀ s n : Nat, reverse (range' s n) = map (s + n - 1 - ·) (range n)
  | _, 0 => rfl
  | s, n + 1 => by
    rw [range'_1_concat, reverse_append, range_succ_eq_map,
      show s + (n + 1) - 1 = s + n from rfl, map, map_map]
    simp [reverse_range', Nat.sub_right_comm, Nat.sub_sub]

Proof state:
s n : Nat
⊢ (range' s (n + 1)).reverse = map (fun x => s + (n + 1) - 1 - x) (range (n + 1))

Tactic:
rw [range'_1_concat, reverse_append, range_succ_eq_map,
  show s + (n + 1) - 1 = s + n from rfl, map, map_map]

Result:
s n : Nat
⊢ [s + n].reverse ++ (range' s n).reverse = (s + n - 0) :: map ((fun x => s + n - x) ∘ succ) (range n)

Proof state:
s n : Nat
⊢ [s + n].reverse ++ (range' s n).reverse = (s + n - 0) :: map ((fun x => s + n - x) ∘ succ) (range n)

Tactic:
simp [reverse_range', Nat.sub_right_comm, Nat.sub_sub]

Result:
no goals
-- Mathlib/RingTheory/Kaehler/CotangentComplex.lean
lemma Hom.sub_one_tmul (f g : Hom P P') (x) :
    f.sub g (1 ⊗ₜ .D _ _ x) = Cotangent.mk (f.subToKer g x)

Proof state:
R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
P : Extension R S
R' : Type u'
S' : Type v'
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing S'
inst✝⁵ : Algebra R' S'
P' : Extension R' S'
inst✝⁴ : Algebra R R'
inst✝³ : Algebra S S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
f g : P.Hom P'
x : P.Ring
⊢ (f.sub g) (1 ⊗ₜ[P.Ring] (D R P.Ring) x) = Cotangent.mk ((f.subToKer g) x)

Tactic:
simp only [sub, LinearMap.liftBaseChange_tmul, Derivation.liftKaehlerDifferential_comp_D,
  Derivation.mk_coe, LinearMap.coe_comp, LinearMap.coe_restrictScalars, Function.comp_apply,
  one_smul]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Sphere/Basic.lean
theorem Cospherical.affineIndependent_of_mem_of_ne {s : Set P} (hs : Cospherical s) {p₁ p₂ p₃ : P}
    (h₁ : p₁ ∈ s) (h₂ : p₂ ∈ s) (h₃ : p₃ ∈ s) (h₁₂ : p₁ ≠ p₂) (h₁₃ : p₁ ≠ p₃) (h₂₃ : p₂ ≠ p₃) :
    AffineIndependent ℝ ![p₁, p₂, p₃]

Proof state:
case refine_1
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
hs : Cospherical s
p₁ p₂ p₃ : P
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
h₃ : p₃ ∈ s
h₁₂ : p₁ ≠ p₂
h₁₃ : p₁ ≠ p₃
h₂₃ : p₂ ≠ p₃
⊢ Set.range ![p₁, p₂, p₃] ⊆ s

Tactic:
simp [h₁, h₂, h₃, Set.insert_subset_iff]

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
hs : Cospherical s
p₁ p₂ p₃ : P
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
h₃ : p₃ ∈ s
h₁₂ : p₁ ≠ p₂
h₁₃ : p₁ ≠ p₃
h₂₃ : p₂ ≠ p₃
⊢ AffineIndependent ℝ ![p₁, p₂, p₃]

Tactic:
refine hs.affineIndependent ?_ ?_

Result:
case refine_1
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
hs : Cospherical s
p₁ p₂ p₃ : P
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
h₃ : p₃ ∈ s
h₁₂ : p₁ ≠ p₂
h₁₃ : p₁ ≠ p₃
h₂₃ : p₂ ≠ p₃
⊢ Set.range ![p₁, p₂, p₃] ⊆ s

case refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
hs : Cospherical s
p₁ p₂ p₃ : P
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
h₃ : p₃ ∈ s
h₁₂ : p₁ ≠ p₂
h₁₃ : p₁ ≠ p₃
h₂₃ : p₂ ≠ p₃
⊢ Function.Injective ![p₁, p₂, p₃]

Proof state:
case refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
hs : Cospherical s
p₁ p₂ p₃ : P
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
h₃ : p₃ ∈ s
h₁₂ : p₁ ≠ p₂
h₁₃ : p₁ ≠ p₃
h₂₃ : p₂ ≠ p₃
⊢ Function.Injective ![p₁, p₂, p₃]

Tactic:
erw [Fin.cons_injective_iff, Fin.cons_injective_iff]

Result:
case refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
hs : Cospherical s
p₁ p₂ p₃ : P
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
h₃ : p₃ ∈ s
h₁₂ : p₁ ≠ p₂
h₁₃ : p₁ ≠ p₃
h₂₃ : p₂ ≠ p₃
⊢ p₁ ∉ Set.range ![p₂, p₃] ∧ p₂ ∉ Set.range ![p₃] ∧ Function.Injective ![p₃]

Proof state:
case refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
hs : Cospherical s
p₁ p₂ p₃ : P
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
h₃ : p₃ ∈ s
h₁₂ : p₁ ≠ p₂
h₁₃ : p₁ ≠ p₃
h₂₃ : p₂ ≠ p₃
⊢ p₁ ∉ Set.range ![p₂, p₃] ∧ p₂ ∉ Set.range ![p₃] ∧ Function.Injective ![p₃]

Tactic:
simp [h₁₂, h₁₃, h₂₃, Function.Injective, eq_iff_true_of_subsingleton]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem mk_emptyCollection_iff {α : Type u} {s : Set α} : #s = 0 ↔ s = ∅

Proof state:
case mpr
α : Type u
⊢ #↑∅ = 0

Tactic:
exact mk_emptyCollection _

Result:
no goals

Proof state:
case mp
α : Type u
s : Set α
h : #↑s = 0
⊢ s = ∅

Tactic:
rw [mk_eq_zero_iff] at h

Result:
case mp
α : Type u
s : Set α
h : IsEmpty ↑s
⊢ s = ∅

Proof state:
case mpr
α : Type u
s : Set α
⊢ s = ∅ → #↑s = 0

Tactic:
rintro rfl

Result:
case mpr
α : Type u
⊢ #↑∅ = 0

Proof state:
case mp
α : Type u
s : Set α
h : IsEmpty ↑s
⊢ s = ∅

Tactic:
exact eq_empty_iff_forall_not_mem.2 fun x hx => h.elim' ⟨x, hx⟩

Result:
no goals

Proof state:
case mp
α : Type u
s : Set α
⊢ #↑s = 0 → s = ∅

Tactic:
intro h

Result:
case mp
α : Type u
s : Set α
h : #↑s = 0
⊢ s = ∅

Proof state:
α : Type u
s : Set α
⊢ #↑s = 0 ↔ s = ∅

Tactic:
constructor

Result:
case mp
α : Type u
s : Set α
⊢ #↑s = 0 → s = ∅

case mpr
α : Type u
s : Set α
⊢ s = ∅ → #↑s = 0
-- Mathlib/RingTheory/PowerSeries/Inverse.lean
theorem ker_coeff_eq_max_ideal : RingHom.ker (constantCoeff k) = maximalIdeal _ :=
  Ideal.ext fun _ ↦ by
    rw [RingHom.mem_ker, maximalIdeal_eq_span_X, Ideal.mem_span_singleton, X_dvd_iff]

Proof state:
k : Type u_2
inst✝ : Field k
x✝ : k⟦X⟧
⊢ x✝ ∈ RingHom.ker (constantCoeff k) ↔ x✝ ∈ maximalIdeal k⟦X⟧

Tactic:
rw [RingHom.mem_ker, maximalIdeal_eq_span_X, Ideal.mem_span_singleton, X_dvd_iff]

Result:
no goals
-- Mathlib/GroupTheory/Coset/Defs.lean
theorem mk_mul_of_mem (a : α) (hb : b ∈ s) : (mk (a * b) : α ⧸ s) = mk a

Proof state:
α : Type u_1
inst✝ : Group α
s : Subgroup α
b a : α
hb : b ∈ s
⊢ ↑(a * b) = ↑a

Tactic:
rwa [QuotientGroup.eq, mul_inv_rev, inv_mul_cancel_right, s.inv_mem_iff]

Result:
no goals
-- Mathlib/Algebra/Order/Hom/Monoid.lean
theorem toMonoidWithZeroHom_injective : Injective (toMonoidWithZeroHom : _ → α →*₀ β) :=
  fun f g h => ext <| by convert DFunLike.ext_iff.1 h using 0

Proof state:
α : Type u_2
β : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : MulZeroOneClass α
inst✝ : MulZeroOneClass β
f g : α →*₀o β
h : f.toMonoidWithZeroHom = g.toMonoidWithZeroHom
⊢ ∀ (a : α), f a = g a

Tactic:
convert DFunLike.ext_iff.1 h using 0

Result:
no goals
-- Mathlib/Probability/Kernel/Defs.lean
lemma isFiniteKernel_of_le {κ ν : Kernel α β} [hν : IsFiniteKernel ν] (hκν : κ ≤ ν) :
    IsFiniteKernel κ

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ ν : Kernel α β
hν : IsFiniteKernel ν
hκν : κ ≤ ν
⊢ IsFiniteKernel κ

Tactic:
refine ⟨hν.bound, hν.bound_lt_top, fun a ↦ (hκν _ _).trans (Kernel.measure_le_bound ν a Set.univ)⟩

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem subsingleton_iff_subsingleton : Subsingleton R[X] ↔ Subsingleton R :=
  ⟨@Injective.subsingleton _ _ _ C_injective, by
    intro
    infer_instance⟩

Proof state:
R : Type u
inst✝ : Semiring R
a✝ : Subsingleton R
⊢ Subsingleton R[X]

Tactic:
infer_instance

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
⊢ Subsingleton R → Subsingleton R[X]

Tactic:
intro

Result:
R : Type u
inst✝ : Semiring R
a✝ : Subsingleton R
⊢ Subsingleton R[X]
-- Mathlib/CategoryTheory/Category/Basic.lean
theorem cancel_epi_assoc_iff (f : X ⟶ Y) [Epi f] {g h : Y ⟶ Z} {W : C} {k l : Z ⟶ W} :
    (f ≫ g) ≫ k = (f ≫ h) ≫ l ↔ g ≫ k = h ≫ l :=
  ⟨fun p => (cancel_epi f).1 <| by simpa using p, fun p => by simp only [Category.assoc, p]⟩

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
inst✝ : Epi f
g h : Y ⟶ Z
W : C
k l : Z ⟶ W
p : g ≫ k = h ≫ l
⊢ (f ≫ g) ≫ k = (f ≫ h) ≫ l

Tactic:
simp only [Category.assoc, p]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
inst✝ : Epi f
g h : Y ⟶ Z
W : C
k l : Z ⟶ W
p : (f ≫ g) ≫ k = (f ≫ h) ≫ l
⊢ f ≫ g ≫ k = f ≫ h ≫ l

Tactic:
simpa using p

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem right_distrib (n m k : Nat) : (n + m) * k = n * k + m * k

Proof state:
n m k : Nat
⊢ k * n + k * m = n * k + m * k

Tactic:
simp [Nat.mul_comm]

Result:
no goals

Proof state:
n m k : Nat
⊢ (n + m) * k = n * k + m * k

Tactic:
rw [Nat.mul_comm, Nat.left_distrib]

Result:
n m k : Nat
⊢ k * n + k * m = n * k + m * k
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sort/Lemmas.lean
theorem splitInTwo_cons_cons_zipIdx_snd (i : Nat) (l : List α) :
    (splitInTwo ⟨(a, i) :: (b, i+1) :: l.zipIdx (i+2), rfl⟩).2.1 =
      (splitInTwo ⟨a :: b :: l, rfl⟩).2.1.zipIdx (i+(l.length+3)/2)

Proof state:
case h
α : Type u_1
a b : α
i : Nat
l : List α
j : Nat
⊢ (drop ((l.length + 1 + 1 + 1) / 2) ((a, i) :: (b, i + 1) :: l.zipIdx (i + 2)))[j]? =
    ((drop ((l.length + 1 + 1 + 1) / 2) (a :: b :: l)).zipIdx (i + (l.length + 3) / 2))[j]?

Tactic:
rw [getElem?_drop, getElem?_zipIdx, getElem?_drop]

Result:
case h
α : Type u_1
a b : α
i : Nat
l : List α
j : Nat
⊢ ((a, i) :: (b, i + 1) :: l.zipIdx (i + 2))[(l.length + 1 + 1 + 1) / 2 + j]? =
    Option.map (fun a => (a, i + (l.length + 3) / 2 + j)) (a :: b :: l)[(l.length + 1 + 1 + 1) / 2 + j]?
-- Mathlib/SetTheory/Game/PGame.lean
theorem neg_le_iff {x y : PGame} : -y ≤ x ↔ -x ≤ y

Proof state:
x y : PGame
⊢ -y ≤ x ↔ -x ≤ y

Tactic:
rw [← neg_neg x, neg_le_neg_iff, neg_neg]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem norm_fderiv_le_of_lipschitzOn {f : E → F} {x₀ : E} {s : Set E} (hs : s ∈ 𝓝 x₀)
    {C : ℝ≥0} (hlip : LipschitzOnWith C f s) : ‖fderiv 𝕜 f x₀‖ ≤ C

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x₀ : E
s : Set E
hs : s ∈ 𝓝 x₀
C : ℝ≥0
hlip : LipschitzOnWith C f s
⊢ ‖fderiv 𝕜 f x₀‖ ≤ ↑C

Tactic:
refine norm_fderiv_le_of_lip' 𝕜 C.coe_nonneg ?_

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x₀ : E
s : Set E
hs : s ∈ 𝓝 x₀
C : ℝ≥0
hlip : LipschitzOnWith C f s
⊢ ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ ↑C * ‖x - x₀‖

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x₀ : E
s : Set E
hs : s ∈ 𝓝 x₀
C : ℝ≥0
hlip : LipschitzOnWith C f s
⊢ ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ ↑C * ‖x - x₀‖

Tactic:
filter_upwards [hs] with x hx using hlip.norm_sub_le hx (mem_of_mem_nhds hs)

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
protected lemma Monotone.iSup (hf : ∀ i, Monotone (f i)) : Monotone (⨆ i, f i) :=
  Monotone.sSup (by simpa)

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝¹ : Preorder α
inst✝ : CompleteLattice β
f : ι → α → β
hf : ∀ (i : ι), Monotone (f i)
⊢ ∀ f_1 ∈ range fun i => f i, Monotone f_1

Tactic:
simpa

Result:
no goals
-- Mathlib/Topology/Sets/Opens.lean
theorem isCompactElement_iff (s : Opens α) :
    CompleteLattice.IsCompactElement s ↔ IsCompact (s : Set α)

Proof state:
α : Type u_2
inst✝ : TopologicalSpace α
s : Opens α
⊢ (∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ t.sup s_1) ↔
    ∀ {ι : Type u_2} (U : ι → Set α), (∀ (i : ι), IsOpen (U i)) → ↑s ⊆ ⋃ i, U i → ∃ t, ↑s ⊆ ⋃ i ∈ t, U i

Tactic:
refine ⟨?_, fun H ι U hU => ?_⟩

Result:
case refine_1
α : Type u_2
inst✝ : TopologicalSpace α
s : Opens α
⊢ (∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ t.sup s_1) →
    ∀ {ι : Type u_2} (U : ι → Set α), (∀ (i : ι), IsOpen (U i)) → ↑s ⊆ ⋃ i, U i → ∃ t, ↑s ⊆ ⋃ i ∈ t, U i

case refine_2
α : Type u_2
inst✝ : TopologicalSpace α
s : Opens α
H : ∀ {ι : Type u_2} (U : ι → Set α), (∀ (i : ι), IsOpen (U i)) → ↑s ⊆ ⋃ i, U i → ∃ t, ↑s ⊆ ⋃ i ∈ t, U i
ι : Type u_2
U : ι → Opens α
hU : s ≤ iSup U
⊢ ∃ t, s ≤ t.sup U
-- Mathlib/Algebra/Homology/HomotopyCofiber.lean
lemma ext_from_X' (i : ι) (hi : ¬ c.Rel i (c.next i)) {A : C} {f g : X φ i ⟶ A}
    (h : inrX φ i ≫ f = inrX φ i ≫ g) : f = g

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i : ι
hi : ¬c.Rel i (c.next i)
A : C
f g : X φ i ⟶ A
h : inrX φ i ≫ f = inrX φ i ≫ g
⊢ f = g

Tactic:
rw [← cancel_epi (XIso φ i hi).inv]

Result:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i : ι
hi : ¬c.Rel i (c.next i)
A : C
f g : X φ i ⟶ A
h : inrX φ i ≫ f = inrX φ i ≫ g
⊢ (XIso φ i hi).inv ≫ f = (XIso φ i hi).inv ≫ g

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i : ι
hi : ¬c.Rel i (c.next i)
A : C
f g : X φ i ⟶ A
h : inrX φ i ≫ f = inrX φ i ≫ g
⊢ (XIso φ i hi).inv ≫ f = (XIso φ i hi).inv ≫ g

Tactic:
simpa only [inrX, dif_neg hi] using h

Result:
no goals
-- Mathlib/LinearAlgebra/ExteriorPower/Basic.lean
theorem map_comp_ιMulti (f : M →ₗ[R] N) :
    (map n f).compAlternatingMap (ιMulti R n) = (ιMulti R n).compLinearMap f

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
f : M →ₗ[R] N
⊢ (map n f).compAlternatingMap (ιMulti R n) = (ιMulti R n).compLinearMap f

Tactic:
simp only [map, alternatingMapLinearEquiv_comp_ιMulti]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem containsKey_eraseKey_of_false [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)}
    {k a : α} (hka : (k == a) = false) : containsKey a (eraseKey k l) = containsKey a l

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
hka : (k == a) = false
⊢ containsKey a (eraseKey k l) = containsKey a l

Tactic:
simp [containsKey_eq_isSome_getEntry?, getEntry?_eraseKey_of_false hka]

Result:
no goals
-- Mathlib/Order/Filter/Pointwise.lean
theorem pure_smul_pure : (pure a : Filter α) • (pure b : Filter β) = pure (a • b)

Proof state:
α : Type u_2
β : Type u_3
inst✝ : SMul α β
a : α
b : β
⊢ pure a • pure b = pure (a • b)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/Action/Defs.lean
@[to_additive]
lemma IsCentralScalar.unop_smul_eq_smul {M α : Type*} [SMul M α] [SMul Mᵐᵒᵖ α]
    [IsCentralScalar M α] (m : Mᵐᵒᵖ) (a : α) : MulOpposite.unop m • a = m • a

Proof state:
case h
M : Type u_9
α : Type u_10
inst✝² : SMul M α
inst✝¹ : SMul Mᵐᵒᵖ α
inst✝ : IsCentralScalar M α
a : α
X✝ : M
⊢ MulOpposite.unop (MulOpposite.op X✝) • a = MulOpposite.op X✝ • a

Tactic:
exact (IsCentralScalar.op_smul_eq_smul _ a).symm

Result:
no goals

Proof state:
M : Type u_9
α : Type u_10
inst✝² : SMul M α
inst✝¹ : SMul Mᵐᵒᵖ α
inst✝ : IsCentralScalar M α
m : Mᵐᵒᵖ
a : α
⊢ MulOpposite.unop m • a = m • a

Tactic:
induction m

Result:
case h
M : Type u_9
α : Type u_10
inst✝² : SMul M α
inst✝¹ : SMul Mᵐᵒᵖ α
inst✝ : IsCentralScalar M α
a : α
X✝ : M
⊢ MulOpposite.unop (MulOpposite.op X✝) • a = MulOpposite.op X✝ • a
-- Mathlib/Algebra/Homology/HomologySequence.lean
@[reassoc (attr := simp)]
lemma homologyι_opcyclesToCycles :
    K.homologyι i ≫ K.opcyclesToCycles i j = 0

Proof state:
C : Type u_1
ι : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : HasZeroMorphisms C
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
inst✝¹ : K.HasHomology i
inst✝ : K.HasHomology j
⊢ K.homologyι i ≫ K.opcyclesToCycles i j = 0

Tactic:
simp only [← cancel_mono (K.iCycles j), assoc, opcyclesToCycles_iCycles,
  homologyι_comp_fromOpcycles, zero_comp]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Over.lean
theorem eq_top_iff_of_liesOver [P.LiesOver p] : P = ⊤ ↔ p = ⊤

Proof state:
A : Type u_2
inst✝³ : CommSemiring A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra A B
P : Ideal B
p : Ideal A
inst✝ : P.LiesOver p
⊢ P = ⊤ ↔ under A P = ⊤

Tactic:
exact comap_eq_top_iff.symm

Result:
no goals

Proof state:
A : Type u_2
inst✝³ : CommSemiring A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra A B
P : Ideal B
p : Ideal A
inst✝ : P.LiesOver p
⊢ P = ⊤ ↔ p = ⊤

Tactic:
rw [P.over_def p]

Result:
A : Type u_2
inst✝³ : CommSemiring A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra A B
P : Ideal B
p : Ideal A
inst✝ : P.LiesOver p
⊢ P = ⊤ ↔ under A P = ⊤
-- Mathlib/ModelTheory/PartialEquiv.lean
theorem toEquivOfEqTop_toEmbedding {f : M ≃ₚ[L] N} (h_dom : f.dom = ⊤)
    (h_cod : f.cod = ⊤) :
    (toEquivOfEqTop h_dom h_cod).toEmbedding = toEmbeddingOfEqTop h_dom

Proof state:
case mk
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
dom : L.Substructure M
cod : L.Substructure N
g : ↥dom ≃[L] ↥cod
h_dom : { dom := dom, cod := cod, toEquiv := g }.dom = ⊤
h_cod : { dom := dom, cod := cod, toEquiv := g }.cod = ⊤
⊢ (toEquivOfEqTop h_dom h_cod).toEmbedding = toEmbeddingOfEqTop h_dom

Tactic:
cases h_dom

Result:
case mk.refl
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
cod : L.Substructure N
g : ↥{ carrier := Set.univ, fun_mem := ⋯ } ≃[L] ↥cod
h_cod : { dom := { carrier := Set.univ, fun_mem := ⋯ }, cod := cod, toEquiv := g }.cod = ⊤
⊢ (toEquivOfEqTop ⋯ h_cod).toEmbedding = toEmbeddingOfEqTop ⋯

Proof state:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃ₚ[L] N
h_dom : f.dom = ⊤
h_cod : f.cod = ⊤
⊢ (toEquivOfEqTop h_dom h_cod).toEmbedding = toEmbeddingOfEqTop h_dom

Tactic:
rcases f with ⟨dom, cod, g⟩

Result:
case mk
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
dom : L.Substructure M
cod : L.Substructure N
g : ↥dom ≃[L] ↥cod
h_dom : { dom := dom, cod := cod, toEquiv := g }.dom = ⊤
h_cod : { dom := dom, cod := cod, toEquiv := g }.cod = ⊤
⊢ (toEquivOfEqTop h_dom h_cod).toEmbedding = toEmbeddingOfEqTop h_dom

Proof state:
case mk.refl.refl
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : ↥{ carrier := Set.univ, fun_mem := ⋯ } ≃[L] ↥{ carrier := Set.univ, fun_mem := ⋯ }
⊢ (toEquivOfEqTop ⋯ ⋯).toEmbedding = toEmbeddingOfEqTop ⋯

Tactic:
rfl

Result:
no goals

Proof state:
case mk.refl
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
cod : L.Substructure N
g : ↥{ carrier := Set.univ, fun_mem := ⋯ } ≃[L] ↥cod
h_cod : { dom := { carrier := Set.univ, fun_mem := ⋯ }, cod := cod, toEquiv := g }.cod = ⊤
⊢ (toEquivOfEqTop ⋯ h_cod).toEmbedding = toEmbeddingOfEqTop ⋯

Tactic:
cases h_cod

Result:
case mk.refl.refl
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : ↥{ carrier := Set.univ, fun_mem := ⋯ } ≃[L] ↥{ carrier := Set.univ, fun_mem := ⋯ }
⊢ (toEquivOfEqTop ⋯ ⋯).toEmbedding = toEmbeddingOfEqTop ⋯
-- Mathlib/Topology/Irreducible.lean
theorem nonempty_preirreducible_inter [PreirreducibleSpace X] :
    IsOpen s → IsOpen t → s.Nonempty → t.Nonempty → (s ∩ t).Nonempty

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
s t : Set X
inst✝ : PreirreducibleSpace X
⊢ IsOpen s → IsOpen t → s.Nonempty → t.Nonempty → (s ∩ t).Nonempty

Tactic:
simpa only [univ_inter, univ_subset_iff] using
  @PreirreducibleSpace.isPreirreducible_univ X _ _ s t

Result:
no goals
-- Mathlib/LinearAlgebra/Projection.lean
theorem prodEquivOfIsCompl_symm_apply_snd_eq_zero (h : IsCompl p q) {x : E} :
    ((prodEquivOfIsCompl p q h).symm x).2 = 0 ↔ x ∈ p

Proof state:
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : Submodule R E
h : IsCompl p q
x : E
⊢ ((p.prodEquivOfIsCompl q h).symm x).2 = 0 ↔ x ∈ p

Tactic:
conv_rhs => rw [← (prodEquivOfIsCompl p q h).apply_symm_apply x]

Result:
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : Submodule R E
h : IsCompl p q
x : E
⊢ ((p.prodEquivOfIsCompl q h).symm x).2 = 0 ↔ (p.prodEquivOfIsCompl q h) ((p.prodEquivOfIsCompl q h).symm x) ∈ p

Proof state:
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : Submodule R E
h : IsCompl p q
x : E
⊢ ((p.prodEquivOfIsCompl q h).symm x).2 = 0 ↔ (p.prodEquivOfIsCompl q h) ((p.prodEquivOfIsCompl q h).symm x) ∈ p

Tactic:
rw [coe_prodEquivOfIsCompl', Submodule.add_mem_iff_right _ (Submodule.coe_mem _),
  mem_left_iff_eq_zero_of_disjoint h.disjoint]

Result:
no goals
-- Mathlib/Order/KrullDimension.lean
@[simp] -- not as useful as a simp lemma as it looks, due to the coe on the left
lemma height_top_eq_krullDim [OrderTop α] : height (⊤ : α) = krullDim α

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : OrderTop α
⊢ height ⊤ = ⨆ p, ↑p.length

Tactic:
apply le_antisymm

Result:
case a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : OrderTop α
⊢ height ⊤ ≤ ⨆ p, ↑p.length

case a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : OrderTop α
⊢ ⨆ p, ↑p.length ≤ height ⊤

Proof state:
case a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : OrderTop α
⊢ height ⊤ ≤ ⨆ p, ↑p.length

Tactic:
exact height_le fun p _ ↦ le_iSup_of_le p le_rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : OrderTop α
⊢ ↑(height ⊤) = ↑(⨆ p, ↑p.length)

Tactic:
simp only [WithBot.coe_inj]

Result:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : OrderTop α
⊢ height ⊤ = ⨆ p, ↑p.length

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : OrderTop α
⊢ ↑(height ⊤) = krullDim α

Tactic:
rw [krullDim_eq_iSup_length]

Result:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : OrderTop α
⊢ ↑(height ⊤) = ↑(⨆ p, ↑p.length)

Proof state:
case a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : OrderTop α
⊢ ⨆ p, ↑p.length ≤ height ⊤

Tactic:
exact iSup_le fun _ => length_le_height le_top

Result:
no goals