harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Function/LpSpace/DomAct/Basic.lean
theorem smul_Lp_sub (c : Mᵈᵐᵃ) : ∀ f g : Lp E p μ, c • (f - g) = c • f - c • g

Proof state:
case mk.mk.mk.mk
M : Type u_1
α : Type u_3
E : Type u_4
inst✝⁵ : MeasurableSpace M
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝² : SMul M α
inst✝¹ : SMulInvariantMeasure M α μ
inst✝ : MeasurableSMul M α
c : Mᵈᵐᵃ
val✝¹ : α →ₘ[μ] E
a✝¹ : { f // AEStronglyMeasurable f μ }
property✝¹ : Quot.mk (⇑(Measure.aeEqSetoid E μ)) a✝¹ ∈ Lp E p μ
val✝ : α →ₘ[μ] E
a✝ : { f // AEStronglyMeasurable f μ }
property✝ : Quot.mk (⇑(Measure.aeEqSetoid E μ)) a✝ ∈ Lp E p μ
⊢ c • (⟨Quot.mk (⇑(Measure.aeEqSetoid E μ)) a✝¹, property✝¹⟩ - ⟨Quot.mk (⇑(Measure.aeEqSetoid E μ)) a✝, property✝⟩) =
    c • ⟨Quot.mk (⇑(Measure.aeEqSetoid E μ)) a✝¹, property✝¹⟩ - c • ⟨Quot.mk (⇑(Measure.aeEqSetoid E μ)) a✝, property✝⟩

Tactic:
rfl

Result:
no goals

Proof state:
M : Type u_1
α : Type u_3
E : Type u_4
inst✝⁵ : MeasurableSpace M
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝² : SMul M α
inst✝¹ : SMulInvariantMeasure M α μ
inst✝ : MeasurableSMul M α
c : Mᵈᵐᵃ
⊢ ∀ (f g : ↥(Lp E p μ)), c • (f - g) = c • f - c • g

Tactic:
rintro ⟨⟨⟩, _⟩ ⟨⟨⟩, _⟩

Result:
case mk.mk.mk.mk
M : Type u_1
α : Type u_3
E : Type u_4
inst✝⁵ : MeasurableSpace M
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝² : SMul M α
inst✝¹ : SMulInvariantMeasure M α μ
inst✝ : MeasurableSMul M α
c : Mᵈᵐᵃ
val✝¹ : α →ₘ[μ] E
a✝¹ : { f // AEStronglyMeasurable f μ }
property✝¹ : Quot.mk (⇑(Measure.aeEqSetoid E μ)) a✝¹ ∈ Lp E p μ
val✝ : α →ₘ[μ] E
a✝ : { f // AEStronglyMeasurable f μ }
property✝ : Quot.mk (⇑(Measure.aeEqSetoid E μ)) a✝ ∈ Lp E p μ
⊢ c • (⟨Quot.mk (⇑(Measure.aeEqSetoid E μ)) a✝¹, property✝¹⟩ - ⟨Quot.mk (⇑(Measure.aeEqSetoid E μ)) a✝, property✝⟩) =
    c • ⟨Quot.mk (⇑(Measure.aeEqSetoid E μ)) a✝¹, property✝¹⟩ - c • ⟨Quot.mk (⇑(Measure.aeEqSetoid E μ)) a✝, property✝⟩
-- Mathlib/FieldTheory/ChevalleyWarning.lean
theorem char_dvd_card_solutions {f : MvPolynomial σ K} (h : f.totalDegree < Fintype.card σ) :
    p ∣ Fintype.card { x : σ → K // eval x f = 0 }

Proof state:
case h.e'_4.h.h.e'_2.h.a
K : Type u_1
σ : Type u_2
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
f : MvPolynomial σ K
h : f.totalDegree < Fintype.card σ
F : Unit → MvPolynomial σ K := fun x => f
this : ∑ i : Unit, (F i).totalDegree < Fintype.card σ
x✝ : σ → K
⊢ (eval x✝) f = 0 ↔ ∀ i ∈ univ, (eval x✝) (F i) = 0

Tactic:
aesop

Result:
no goals

Proof state:
K : Type u_1
σ : Type u_2
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
f : MvPolynomial σ K
h : f.totalDegree < Fintype.card σ
F : Unit → MvPolynomial σ K := fun x => f
this : ∑ i : Unit, (F i).totalDegree < Fintype.card σ
⊢ p ∣ Fintype.card { x // (eval x) f = 0 }

Tactic:
convert char_dvd_card_solutions_of_sum_lt p this

Result:
case h.e'_4.h.h.e'_2.h.a
K : Type u_1
σ : Type u_2
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
f : MvPolynomial σ K
h : f.totalDegree < Fintype.card σ
F : Unit → MvPolynomial σ K := fun x => f
this : ∑ i : Unit, (F i).totalDegree < Fintype.card σ
x✝ : σ → K
⊢ (eval x✝) f = 0 ↔ ∀ i ∈ univ, (eval x✝) (F i) = 0

Proof state:
K : Type u_1
σ : Type u_2
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
f : MvPolynomial σ K
h : f.totalDegree < Fintype.card σ
⊢ p ∣ Fintype.card { x // (eval x) f = 0 }

Tactic:
let F : Unit → MvPolynomial σ K := fun _ => f

Result:
K : Type u_1
σ : Type u_2
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
f : MvPolynomial σ K
h : f.totalDegree < Fintype.card σ
F : Unit → MvPolynomial σ K := fun x => f
⊢ p ∣ Fintype.card { x // (eval x) f = 0 }

Proof state:
K : Type u_1
σ : Type u_2
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
f : MvPolynomial σ K
h : f.totalDegree < Fintype.card σ
F : Unit → MvPolynomial σ K := fun x => f
⊢ p ∣ Fintype.card { x // (eval x) f = 0 }

Tactic:
have : (∑ i : Unit, (F i).totalDegree) < Fintype.card σ := h

Result:
K : Type u_1
σ : Type u_2
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
f : MvPolynomial σ K
h : f.totalDegree < Fintype.card σ
F : Unit → MvPolynomial σ K := fun x => f
this : ∑ i : Unit, (F i).totalDegree < Fintype.card σ
⊢ p ∣ Fintype.card { x // (eval x) f = 0 }
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNorm'_zero (hp0_lt : 0 < q) : eLpNorm' (0 : α → F) q μ = 0

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup F
hp0_lt : 0 < q
⊢ eLpNorm' 0 q μ = 0

Tactic:
simp [eLpNorm'_eq_lintegral_enorm, hp0_lt]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Operations.lean
theorem card_edgeFinset_sup_edge [Fintype (edgeSet (G ⊔ edge s t))] (hn : ¬G.Adj s t) (h : s ≠ t) :
    #(G ⊔ edge s t).edgeFinset = #G.edgeFinset + 1

Proof state:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype ↑(G ⊔ edge s t).edgeSet
hn : ¬G.Adj s t
h : s ≠ t
⊢ #(G ⊔ edge s t).edgeFinset = #G.edgeFinset + 1

Tactic:
rw [G.edgeFinset_sup_edge hn h, card_cons]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {h'} :
    (m.erase a).getKey k h' = m.getKey k (mem_of_mem_erase h h')

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k a : α
h' : k ∈ m.erase a
⊢ (m.erase a).getKey k h' = m.getKey k ⋯

Tactic:
simp_to_raw using Raw₀.getKey_erase ⟨m, _⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem dropWhile_cons_of_pos {a : α} {l : List α} (h : p a) :
    (a :: l).dropWhile p = l.dropWhile p

Proof state:
α : Type u_1
p : α → Bool
a : α
l : List α
h : p a = true
⊢ dropWhile p (a :: l) = dropWhile p l

Tactic:
simp [dropWhile_cons, h]

Result:
no goals
-- Mathlib/RingTheory/Regular/IsSMulRegular.lean
lemma isSMulRegular_on_quot_iff_smul_mem_implies_mem :
    IsSMulRegular (M ⧸ N) r ↔ ∀ x : M, r • x ∈ N → x ∈ N :=
  Iff.trans (isSMulRegular_iff_smul_eq_zero_imp_eq_zero _ r) <|
    Iff.trans N.mkQ_surjective.forall <| by
      simp_rw [← map_smul, N.mkQ_apply, Submodule.Quotient.mk_eq_zero]

Proof state:
R : Type u_1
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
r : R
⊢ (∀ (x : M), r • N.mkQ x = 0 → N.mkQ x = 0) ↔ ∀ (x : M), r • x ∈ N → x ∈ N

Tactic:
simp_rw [← map_smul, N.mkQ_apply, Submodule.Quotient.mk_eq_zero]

Result:
no goals
-- Mathlib/LinearAlgebra/Quotient/Basic.lean
theorem mapQ_zero (h : p ≤ q.comap (0 : M →ₛₗ[τ₁₂] M₂) := (by simp)) :
    p.mapQ q (0 : M →ₛₗ[τ₁₂] M₂) h = 0

Proof state:
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
h : optParam (p ≤ comap 0 q) ⋯
⊢ p.mapQ q 0 h = 0

Tactic:
ext

Result:
case h.h
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
h : optParam (p ≤ comap 0 q) ⋯
x✝ : M
⊢ ((p.mapQ q 0 h).comp p.mkQ) x✝ = (comp 0 p.mkQ) x✝

Proof state:
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' p'' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
⊢ p ≤ comap 0 q

Tactic:
simp

Result:
no goals

Proof state:
case h.h
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
h : optParam (p ≤ comap 0 q) ⋯
x✝ : M
⊢ ((p.mapQ q 0 h).comp p.mkQ) x✝ = (comp 0 p.mkQ) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Range.lean
theorem zipIdx_succ (l : Vector α n) (m : Nat) :
    l.zipIdx (m + 1) = (l.zipIdx m).map (fun ⟨a, i⟩ => (a, i + 1))

Proof state:
case mk
α : Type u_1
m : Nat
l : Array α
⊢ { toArray := l, size_toArray := ⋯ }.zipIdx (m + 1) =
    map
      (fun x =>
        match x with
        | (a, i) => (a, i + 1))
      ({ toArray := l, size_toArray := ⋯ }.zipIdx m)

Tactic:
simp [Array.zipIdx_succ]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
l : Vector α n
m : Nat
⊢ l.zipIdx (m + 1) =
    map
      (fun x =>
        match x with
        | (a, i) => (a, i + 1))
      (l.zipIdx m)

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
m : Nat
l : Array α
⊢ { toArray := l, size_toArray := ⋯ }.zipIdx (m + 1) =
    map
      (fun x =>
        match x with
        | (a, i) => (a, i + 1))
      ({ toArray := l, size_toArray := ⋯ }.zipIdx m)
-- Mathlib/RingTheory/Algebraic/Basic.lean
theorem Algebra.Transcendental.ringHom_of_comp_eq [H : Algebra.Transcendental R A]
    (hf : Function.Surjective f) (hg : Function.Injective g)
    (h : RingHom.comp (algebraMap S B) f = RingHom.comp g (algebraMap R A)) :
    Algebra.Transcendental S B

Proof state:
R : Type u
S : Type u_1
A : Type v
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Ring A
inst✝⁶ : Algebra R A
B : Type u_2
inst✝⁵ : Ring B
inst✝⁴ : Algebra S B
FRS : Type u_3
FAB : Type u_4
inst✝³ : FunLike FRS R S
inst✝² : RingHomClass FRS R S
inst✝¹ : FunLike FAB A B
inst✝ : RingHomClass FAB A B
f : FRS
g : FAB
H : ¬Algebra.IsAlgebraic R A
hf : Function.Surjective ⇑f
hg : Function.Injective ⇑g
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
⊢ ¬Algebra.IsAlgebraic S B

Tactic:
exact fun halg ↦ H (halg.of_ringHom_of_comp_eq f g hf hg h)

Result:
no goals

Proof state:
R : Type u
S : Type u_1
A : Type v
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Ring A
inst✝⁶ : Algebra R A
B : Type u_2
inst✝⁵ : Ring B
inst✝⁴ : Algebra S B
FRS : Type u_3
FAB : Type u_4
inst✝³ : FunLike FRS R S
inst✝² : RingHomClass FRS R S
inst✝¹ : FunLike FAB A B
inst✝ : RingHomClass FAB A B
f : FRS
g : FAB
H : Algebra.Transcendental R A
hf : Function.Surjective ⇑f
hg : Function.Injective ⇑g
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
⊢ Algebra.Transcendental S B

Tactic:
rw [Algebra.transcendental_iff_not_isAlgebraic] at H ⊢

Result:
R : Type u
S : Type u_1
A : Type v
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Ring A
inst✝⁶ : Algebra R A
B : Type u_2
inst✝⁵ : Ring B
inst✝⁴ : Algebra S B
FRS : Type u_3
FAB : Type u_4
inst✝³ : FunLike FRS R S
inst✝² : RingHomClass FRS R S
inst✝¹ : FunLike FAB A B
inst✝ : RingHomClass FAB A B
f : FRS
g : FAB
H : ¬Algebra.IsAlgebraic R A
hf : Function.Surjective ⇑f
hg : Function.Injective ⇑g
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
⊢ ¬Algebra.IsAlgebraic S B
-- Mathlib/Combinatorics/HalesJewett.lean
@[simp] lemma reindex_apply (l : Subspace η α ι) (eη : η ≃ η') (eα : α ≃ α') (eι : ι ≃ ι') (x i) :
    l.reindex eη eα eι x i = eα (l (eα.symm ∘ x ∘ eη) <| eι.symm i)

Proof state:
η : Type u_5
α : Type u_6
ι : Type u_7
η' : Type u_9
α' : Type u_10
ι' : Type u_11
l : Subspace η α ι
eη : η ≃ η'
eα : α ≃ α'
eι : ι ≃ ι'
x : η' → α'
i : ι'
⊢ ↑(l.reindex eη eα eι) x i = eα (↑l (⇑eα.symm ∘ x ∘ ⇑eη) (eι.symm i))

Tactic:
cases h : l.idxFun (eι.symm i) <;> simp [h, reindex, coe_apply]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem zneg_bit1 (n : ZNum) : -n.bit1 = (-n).bitm1

Proof state:
n : ZNum
⊢ -n.bit1 = (-n).bitm1

Tactic:
cases n <;> rfl

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean
@[reassoc (attr := simp)]
lemma cyclesIso_hom_comp_i : h.cyclesIso.hom ≫ h.i = S.iCycles

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h : S.LeftHomologyData
inst✝ : S.HasLeftHomology
⊢ cyclesMap' (𝟙 S) S.leftHomologyData h ≫ h.i = S.leftHomologyData.i

Tactic:
simp only [cyclesMap'_i, id_τ₂, 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
inst✝ : S.HasLeftHomology
⊢ h.cyclesIso.hom ≫ h.i = S.iCycles

Tactic:
dsimp [iCycles, LeftHomologyData.cyclesIso]

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h : S.LeftHomologyData
inst✝ : S.HasLeftHomology
⊢ cyclesMap' (𝟙 S) S.leftHomologyData h ≫ h.i = S.leftHomologyData.i
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem derivative_X_sq : derivative (X ^ 2 : R[X]) = C 2 * X

Proof state:
R : Type u
inst✝ : Semiring R
⊢ derivative (X ^ 2) = C 2 * X

Tactic:
rw [derivative_X_pow, Nat.cast_two, pow_one]

Result:
no goals
-- Mathlib/Algebra/Ring/Parity.lean
@[simp] lemma Odd.mul : Odd a → Odd b → Odd (a * b)

Proof state:
case intro.intro
α : Type u_2
inst✝ : Semiring α
a b : α
⊢ Odd ((2 * a + 1) * (2 * b + 1))

Tactic:
refine ⟨2 * a * b + b + a, ?_⟩

Result:
case intro.intro
α : Type u_2
inst✝ : Semiring α
a b : α
⊢ (2 * a + 1) * (2 * b + 1) = 2 * (2 * a * b + b + a) + 1

Proof state:
case intro.intro
α : Type u_2
inst✝ : Semiring α
a b : α
⊢ (2 * a + 1) * (2 * b + 1) = 2 * (2 * a * b + b + a) + 1

Tactic:
rw [mul_add, add_mul, mul_one, ← add_assoc, one_mul, mul_assoc, ← mul_add, ← mul_add, ← mul_assoc,
  ← Nat.cast_two, ← Nat.cast_comm]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : Semiring α
a b : α
⊢ Odd a → Odd b → Odd (a * b)

Tactic:
rintro ⟨a, rfl⟩ ⟨b, rfl⟩

Result:
case intro.intro
α : Type u_2
inst✝ : Semiring α
a b : α
⊢ Odd ((2 * a + 1) * (2 * b + 1))
-- Mathlib/Data/Set/Prod.lean
theorem prodMap_image_prod (f : α → β) (g : γ → δ) (s : Set α) (t : Set γ) :
    (Prod.map f g) '' (s ×ˢ t) = (f '' s) ×ˢ (g '' t)

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β
g : γ → δ
s : Set α
t : Set γ
x✝ : β × δ
⊢ x✝ ∈ Prod.map f g '' s ×ˢ t ↔ x✝ ∈ (f '' s) ×ˢ (g '' t)

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β
g : γ → δ
s : Set α
t : Set γ
⊢ Prod.map f g '' s ×ˢ t = (f '' s) ×ˢ (g '' t)

Tactic:
ext

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β
g : γ → δ
s : Set α
t : Set γ
x✝ : β × δ
⊢ x✝ ∈ Prod.map f g '' s ×ˢ t ↔ x✝ ∈ (f '' s) ×ˢ (g '' t)
-- Mathlib/CategoryTheory/ChosenFiniteProducts.lean
@[reassoc, simp]
lemma comp_lift {V W X Y : C} (f : V ⟶ W) (g : W ⟶ X) (h : W ⟶ Y) :
    f ≫ lift g h = lift (f ≫ g) (f ≫ h)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ChosenFiniteProducts C
V W X Y : C
f : V ⟶ W
g : W ⟶ X
h : W ⟶ Y
⊢ f ≫ lift g h = lift (f ≫ g) (f ≫ h)

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Topology/MetricSpace/Defs.lean
theorem dist_pos {x y : γ} : 0 < dist x y ↔ x ≠ y

Proof state:
γ : Type w
inst✝ : MetricSpace γ
x y : γ
⊢ 0 < dist x y ↔ x ≠ y

Tactic:
simpa only [not_le] using not_congr dist_le_zero

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem setIfInBounds_append_right {s : Vector α n} {t : Vector α m} {i : Nat} {x : α}
    (h : n ≤ i) :
    (s ++ t).setIfInBounds i x = s ++ t.setIfInBounds (i - n) x

Proof state:
α : Type u_1
n m : Nat
s : Vector α n
t : Vector α m
i : Nat
x : α
h : n ≤ i
⊢ ¬i < n

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
n m : Nat
s : Vector α n
t : Vector α m
i : Nat
x : α
h : n ≤ i
⊢ (s ++ t).setIfInBounds i x = s ++ t.setIfInBounds (i - n) x

Tactic:
rw [setIfInBounds_append, if_neg (by omega)]

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/TruncGEHomology.lean
/-- `K.restrictionToTruncGE' e` is a quasi-isomorphism in degrees that are not at the boundary. -/
lemma quasiIsoAt_restrictionToTruncGE' (hj : ¬ e.BoundaryGE j)
    [(K.restriction e).HasHomology j] [(K.truncGE' e).HasHomology j] :
    QuasiIsoAt (K.restrictionToTruncGE' e) j

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{u_4, u_3} C
inst✝⁴ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
j : ι
hj : ¬e.BoundaryGE j
inst✝¹ : (K.restriction e).HasHomology j
inst✝ : (K.truncGE' e).HasHomology j
φ : (shortComplexFunctor C c j).obj (K.restriction e) ⟶ (shortComplexFunctor C c j).obj (K.truncGE' e) :=
  (shortComplexFunctor C c j).map (K.restrictionToTruncGE' e)
⊢ ShortComplex.QuasiIso ((shortComplexFunctor C c j).map (K.restrictionToTruncGE' e))

Tactic:
have : Epi φ.τ₁ := by dsimp [φ]; infer_instance

Result:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{u_4, u_3} C
inst✝⁴ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
j : ι
hj : ¬e.BoundaryGE j
inst✝¹ : (K.restriction e).HasHomology j
inst✝ : (K.truncGE' e).HasHomology j
φ : (shortComplexFunctor C c j).obj (K.restriction e) ⟶ (shortComplexFunctor C c j).obj (K.truncGE' e) :=
  (shortComplexFunctor C c j).map (K.restrictionToTruncGE' e)
this : Epi φ.τ₁
⊢ ShortComplex.QuasiIso ((shortComplexFunctor C c j).map (K.restrictionToTruncGE' e))
-- Mathlib/Data/Nat/Size.lean
theorem shiftLeft'_ne_zero_left (b) {m} (h : m ≠ 0) (n) : shiftLeft' b m n ≠ 0

Proof state:
b : Bool
m : ℕ
h : m ≠ 0
n : ℕ
⊢ shiftLeft' b m n ≠ 0

Tactic:
induction n <;> simp [bit_ne_zero, shiftLeft', *]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem div_one (a : Ordinal) : a / 1 = a

Proof state:
a : Ordinal.{u_4}
⊢ a / 1 = a

Tactic:
simpa only [one_mul] using mul_div_cancel a Ordinal.one_ne_zero

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Symmetric/FundamentalTheorem.lean
lemma esymmAlgHom_zero : esymmAlgHomMonomial σ (0 : Fin n →₀ ℕ) r = C r

Proof state:
σ : Type u_1
R : Type u_3
n : ℕ
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
r : R
⊢ esymmAlgHomMonomial σ 0 r = C r

Tactic:
rw [esymmAlgHomMonomial, monomial_zero', esymmAlgHom_apply, aeval_C, algebraMap_eq]

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/Jordan.lean
theorem eq_of_posPart_eq_posPart {j₁ j₂ : JordanDecomposition α}
    (hj : j₁.posPart = j₂.posPart) (hj' : j₁.toSignedMeasure = j₂.toSignedMeasure) : j₁ = j₂

Proof state:
case negPart
α : Type u_1
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.posPart = j₂.posPart
hj' : j₁.posPart.toSignedMeasure - j₁.negPart.toSignedMeasure = j₂.posPart.toSignedMeasure - j₂.negPart.toSignedMeasure
⊢ j₁.negPart.toSignedMeasure = j₂.negPart.toSignedMeasure

Tactic:
simp_rw [hj, sub_right_inj] at hj'

Result:
case negPart
α : Type u_1
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.posPart = j₂.posPart
hj' : j₁.negPart.toSignedMeasure = j₂.negPart.toSignedMeasure
⊢ j₁.negPart.toSignedMeasure = j₂.negPart.toSignedMeasure

Proof state:
case negPart
α : Type u_1
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.posPart = j₂.posPart
hj' : j₁.negPart.toSignedMeasure = j₂.negPart.toSignedMeasure
⊢ j₁.negPart.toSignedMeasure = j₂.negPart.toSignedMeasure

Tactic:
exact hj'

Result:
no goals

Proof state:
case negPart
α : Type u_1
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.posPart = j₂.posPart
hj' : j₁.toSignedMeasure = j₂.toSignedMeasure
⊢ j₁.negPart = j₂.negPart

Tactic:
rw [← toSignedMeasure_eq_toSignedMeasure_iff]

Result:
case negPart
α : Type u_1
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.posPart = j₂.posPart
hj' : j₁.toSignedMeasure = j₂.toSignedMeasure
⊢ j₁.negPart.toSignedMeasure = j₂.negPart.toSignedMeasure

Proof state:
case negPart
α : Type u_1
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.posPart = j₂.posPart
hj' : j₁.toSignedMeasure = j₂.toSignedMeasure
⊢ j₁.negPart.toSignedMeasure = j₂.negPart.toSignedMeasure

Tactic:
unfold toSignedMeasure at hj'

Result:
case negPart
α : Type u_1
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.posPart = j₂.posPart
hj' : j₁.posPart.toSignedMeasure - j₁.negPart.toSignedMeasure = j₂.posPart.toSignedMeasure - j₂.negPart.toSignedMeasure
⊢ j₁.negPart.toSignedMeasure = j₂.negPart.toSignedMeasure

Proof state:
case posPart
α : Type u_1
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.posPart = j₂.posPart
hj' : j₁.toSignedMeasure = j₂.toSignedMeasure
⊢ j₁.posPart = j₂.posPart

Tactic:
exact hj

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.posPart = j₂.posPart
hj' : j₁.toSignedMeasure = j₂.toSignedMeasure
⊢ j₁ = j₂

Tactic:
ext1

Result:
case posPart
α : Type u_1
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.posPart = j₂.posPart
hj' : j₁.toSignedMeasure = j₂.toSignedMeasure
⊢ j₁.posPart = j₂.posPart

case negPart
α : Type u_1
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.posPart = j₂.posPart
hj' : j₁.toSignedMeasure = j₂.toSignedMeasure
⊢ j₁.negPart = j₂.negPart
-- Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean
theorem directSum_symm_lof_tmul (i₁ : ι₁) (m₁ : M₁ i₁) (i₂ : ι₂) (m₂ : M₂ i₂) :
    (TensorProduct.directSum R S M₁ M₂).symm
      (DirectSum.lof S (ι₁ × ι₂) (fun i => M₁ i.1 ⊗[R] M₂ i.2) (i₁, i₂) (m₁ ⊗ₜ m₂)) =
      (DirectSum.lof S ι₁ M₁ i₁ m₁ ⊗ₜ DirectSum.lof R ι₂ M₂ i₂ m₂)

Proof state:
R : Type u
inst✝¹⁰ : CommSemiring R
S : Type u_1
inst✝⁹ : Semiring S
inst✝⁸ : Algebra R S
ι₁ : Type v₁
ι₂ : Type v₂
inst✝⁷ : DecidableEq ι₁
inst✝⁶ : DecidableEq ι₂
M₁ : ι₁ → Type w₁
M₂ : ι₂ → Type w₂
inst✝⁵ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst✝⁴ : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝¹ : (i₁ : ι₁) → Module S (M₁ i₁)
inst✝ : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)
i₁ : ι₁
m₁ : M₁ i₁
i₂ : ι₂
m₂ : M₂ i₂
⊢ (TensorProduct.directSum R S M₁ M₂).symm ((lof S (ι₁ × ι₂) (fun i => M₁ i.1 ⊗[R] M₂ i.2) (i₁, i₂)) (m₁ ⊗ₜ[R] m₂)) =
    (lof S ι₁ M₁ i₁) m₁ ⊗ₜ[R] (lof R ι₂ M₂ i₂) m₂

Tactic:
rw [LinearEquiv.symm_apply_eq, directSum_lof_tmul_lof]

Result:
no goals
-- Mathlib/Topology/Connected/Basic.lean
theorem isConnected_connectedComponentIn_iff {x : α} {F : Set α} :
    IsConnected (connectedComponentIn F x) ↔ x ∈ F

Proof state:
α : Type u
inst✝ : TopologicalSpace α
x : α
F : Set α
⊢ IsConnected (connectedComponentIn F x) ↔ x ∈ F

Tactic:
simp_rw [← connectedComponentIn_nonempty_iff, IsConnected, isPreconnected_connectedComponentIn,
  and_true]

Result:
no goals
-- Mathlib/Algebra/Ring/CentroidHom.lean
theorem cancel_left {g f₁ f₂ : CentroidHom α} (hg : Injective g) :
    g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h ↦ ext fun a ↦ hg <| by rw [← comp_apply, h, comp_apply], congr_arg _⟩

Proof state:
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
g f₁ f₂ : CentroidHom α
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
rw [← comp_apply, h, comp_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem_setIfInBounds_self (as : Array α) {i : Nat} (v : α) (h : _) :
    (as.setIfInBounds i v)[i]'h = v

Proof state:
α : Type u_1
as : Array α
i : Nat
v : α
h : i < (as.setIfInBounds i v).size
⊢ (as.setIfInBounds i v)[i] = v

Tactic:
simp at h

Result:
α : Type u_1
as : Array α
i : Nat
v : α
h✝ : i < (as.setIfInBounds i v).size
h : i < as.size
⊢ (as.setIfInBounds i v)[i] = v

Proof state:
α : Type u_1
as : Array α
i : Nat
v : α
h✝ : i < (as.setIfInBounds i v).size
h : i < as.size
⊢ (as.setIfInBounds i v)[i] = v

Tactic:
simp only [setIfInBounds, h, ↓reduceDIte, getElem_set_self]

Result:
no goals