harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKeyD_insertManyIfNewUnit_list_of_contains [EquivBEq α] [LawfulHashable α]
    (h : m.1.WF) {l : List α} {k fallback : α} :
    m.contains k → getKeyD (insertManyIfNewUnit m l).1 k fallback = getKeyD m k fallback

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw₀ α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
l : List α
k fallback : α
⊢ m.contains k = true → (insertManyIfNewUnit m l).val.getKeyD k fallback = m.getKeyD k fallback

Tactic:
simp_to_model [Const.insertManyIfNewUnit] using List.getKeyD_insertListIfNewUnit_of_contains

Result:
no goals
-- Mathlib/Algebra/Group/Hom/Defs.lean
@[to_additive]
lemma map_comp_div' [DivInvMonoid G] [DivInvMonoid H] [MonoidHomClass F G H] (f : F)
    (hf : ∀ a, f a⁻¹ = (f a)⁻¹) (g h : ι → G) : f ∘ (g / h) = f ∘ g / f ∘ h

Proof state:
ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : DivInvMonoid G
inst✝¹ : DivInvMonoid H
inst✝ : MonoidHomClass F G H
f : F
hf : ∀ (a : G), f a⁻¹ = (f a)⁻¹
g h : ι → G
⊢ ⇑f ∘ (g / h) = ⇑f ∘ g / ⇑f ∘ h

Tactic:
ext

Result:
case h
ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : DivInvMonoid G
inst✝¹ : DivInvMonoid H
inst✝ : MonoidHomClass F G H
f : F
hf : ∀ (a : G), f a⁻¹ = (f a)⁻¹
g h : ι → G
x✝ : ι
⊢ (⇑f ∘ (g / h)) x✝ = (⇑f ∘ g / ⇑f ∘ h) x✝

Proof state:
case h
ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : DivInvMonoid G
inst✝¹ : DivInvMonoid H
inst✝ : MonoidHomClass F G H
f : F
hf : ∀ (a : G), f a⁻¹ = (f a)⁻¹
g h : ι → G
x✝ : ι
⊢ (⇑f ∘ (g / h)) x✝ = (⇑f ∘ g / ⇑f ∘ h) x✝

Tactic:
simp [map_div' f hf]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem mem_support_iff_mem_support_of_mem_cycleFactorsFinset {g : Equiv.Perm α} {x : α} :
    x ∈ g.support ↔ ∃ c ∈ g.cycleFactorsFinset, x ∈ c.support

Proof state:
case right
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x : α
h : x ∈ g.support
⊢ x ∈ (g.cycleOf x).support

Tactic:
rw [mem_support_cycleOf_iff]

Result:
case right
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x : α
h : x ∈ g.support
⊢ g.SameCycle x x ∧ x ∈ g.support

Proof state:
case mpr.intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x : α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
hx : x ∈ c.support
⊢ x ∈ g.support

Tactic:
exact mem_cycleFactorsFinset_support_le hc hx

Result:
no goals

Proof state:
case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x : α
⊢ x ∈ g.support → ∃ c ∈ g.cycleFactorsFinset, x ∈ c.support

Tactic:
intro h

Result:
case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x : α
h : x ∈ g.support
⊢ ∃ c ∈ g.cycleFactorsFinset, x ∈ c.support

Proof state:
case right
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x : α
h : x ∈ g.support
⊢ g.SameCycle x x ∧ x ∈ g.support

Tactic:
exact ⟨SameCycle.refl g x, h⟩

Result:
no goals

Proof state:
case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x : α
h : x ∈ g.support
⊢ ∃ c ∈ g.cycleFactorsFinset, x ∈ c.support

Tactic:
use g.cycleOf x, cycleOf_mem_cycleFactorsFinset_iff.mpr h

Result:
case right
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x : α
h : x ∈ g.support
⊢ x ∈ (g.cycleOf x).support

Proof state:
case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x : α
⊢ (∃ c ∈ g.cycleFactorsFinset, x ∈ c.support) → x ∈ g.support

Tactic:
rintro ⟨c, hc, hx⟩

Result:
case mpr.intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x : α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
hx : x ∈ c.support
⊢ x ∈ g.support

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x : α
⊢ x ∈ g.support ↔ ∃ c ∈ g.cycleFactorsFinset, x ∈ c.support

Tactic:
constructor

Result:
case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x : α
⊢ x ∈ g.support → ∃ c ∈ g.cycleFactorsFinset, x ∈ c.support

case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x : α
⊢ (∃ c ∈ g.cycleFactorsFinset, x ∈ c.support) → x ∈ g.support
-- Mathlib/GroupTheory/NoncommCoprod.lean
theorem comp_noncommCoprod {Q : Type*} [Monoid Q] (h : P →* Q) :
    h.comp (f.noncommCoprod g comm) =
      (h.comp f).noncommCoprod (h.comp g) (fun m n ↦ (comm m n).map h) :=
  ext fun x => by simp

Proof state:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : Monoid P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
Q : Type u_4
inst✝ : Monoid Q
h : P →* Q
x : M × N
⊢ (h.comp (f.noncommCoprod g comm)) x = ((h.comp f).noncommCoprod (h.comp g) ⋯) x

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem leadingCoeff_add_of_degree_lt (h : degree p < degree q) :
    leadingCoeff (p + q) = leadingCoeff q

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.degree < q.degree
this : p.coeff q.natDegree = 0
⊢ (p + q).leadingCoeff = q.leadingCoeff

Tactic:
simp only [leadingCoeff, natDegree_eq_of_degree_eq (degree_add_eq_right_of_degree_lt h), this,
  coeff_add, zero_add]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.degree < q.degree
⊢ (p + q).leadingCoeff = q.leadingCoeff

Tactic:
have : coeff p (natDegree q) = 0 := coeff_natDegree_eq_zero_of_degree_lt h

Result:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.degree < q.degree
this : p.coeff q.natDegree = 0
⊢ (p + q).leadingCoeff = q.leadingCoeff
-- Mathlib/Geometry/Euclidean/Circumcenter.lean
theorem sum_centroidWeightsWithCircumcenter {n : ℕ} {fs : Finset (Fin (n + 1))} (h : fs.Nonempty) :
    ∑ i, centroidWeightsWithCircumcenter fs i = 1

Proof state:
n : ℕ
fs : Finset (Fin (n + 1))
h : fs.Nonempty
⊢ (∑ x : Fin (n + 1), if x ∈ fs then (↑(#fs))⁻¹ else 0) = ∑ i : Fin (n + 1), (↑fs).indicator (centroidWeights ℝ fs) i

Tactic:
rcongr

Result:
no goals

Proof state:
n : ℕ
fs : Finset (Fin (n + 1))
h : fs.Nonempty
⊢ ∑ i : PointsWithCircumcenterIndex n, centroidWeightsWithCircumcenter fs i = 1

Tactic:
simp_rw [sum_pointsWithCircumcenter, centroidWeightsWithCircumcenter, add_zero, ←
  fs.sum_centroidWeights_eq_one_of_nonempty ℝ h, ← sum_indicator_subset _ fs.subset_univ]

Result:
n : ℕ
fs : Finset (Fin (n + 1))
h : fs.Nonempty
⊢ (∑ x : Fin (n + 1), if x ∈ fs then (↑(#fs))⁻¹ else 0) = ∑ i : Fin (n + 1), (↑fs).indicator (centroidWeights ℝ fs) i
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem ae_eq_zero_of_eLpNorm'_eq_zero {f : α → E} (hq0 : 0 ≤ q) (hf : AEStronglyMeasurable f μ)
    (h : eLpNorm' f q μ = 0) : f =ᵐ[μ] 0

Proof state:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hq0 : 0 ≤ q
hf : AEStronglyMeasurable f μ
h : eLpNorm' f q μ = 0
⊢ f =ᶠ[ae μ] 0

Tactic:
simp only [eLpNorm'_eq_lintegral_enorm, lintegral_eq_zero_iff' (hf.enorm.pow_const q), one_div,
  ENNReal.rpow_eq_zero_iff, inv_pos, inv_neg'', hq0.not_lt, and_false, or_false] at h

Result:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hq0 : 0 ≤ q
hf : AEStronglyMeasurable f μ
h : (fun a => ‖f a‖ₑ ^ q) =ᶠ[ae μ] 0 ∧ 0 < q
⊢ f =ᶠ[ae μ] 0

Proof state:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hq0 : 0 ≤ q
hf : AEStronglyMeasurable f μ
h : (fun a => ‖f a‖ₑ ^ q) =ᶠ[ae μ] 0 ∧ 0 < q
⊢ f =ᶠ[ae μ] 0

Tactic:
refine h.left.mono fun x hx ↦ ?_

Result:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hq0 : 0 ≤ q
hf : AEStronglyMeasurable f μ
h : (fun a => ‖f a‖ₑ ^ q) =ᶠ[ae μ] 0 ∧ 0 < q
x : α
hx : (fun a => ‖f a‖ₑ ^ q) x = 0 x
⊢ f x = 0 x

Proof state:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hq0 : 0 ≤ q
hf : AEStronglyMeasurable f μ
h : (fun a => ‖f a‖ₑ ^ q) =ᶠ[ae μ] 0 ∧ 0 < q
x : α
hx : (fun a => ‖f a‖ₑ ^ q) x = 0 x
⊢ f x = 0 x

Tactic:
simp only [Pi.zero_apply, ENNReal.rpow_eq_zero_iff, enorm_eq_zero, enorm_ne_top, false_and,
  or_false] at hx

Result:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hq0 : 0 ≤ q
hf : AEStronglyMeasurable f μ
h : (fun a => ‖f a‖ₑ ^ q) =ᶠ[ae μ] 0 ∧ 0 < q
x : α
hx : f x = 0 ∧ 0 < q
⊢ f x = 0 x

Proof state:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hq0 : 0 ≤ q
hf : AEStronglyMeasurable f μ
h : (fun a => ‖f a‖ₑ ^ q) =ᶠ[ae μ] 0 ∧ 0 < q
x : α
hx : f x = 0 ∧ 0 < q
⊢ f x = 0 x

Tactic:
exact hx.1

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Rename.lean
theorem eval₂_rename : (rename k p).eval₂ f g = p.eval₂ f (g ∘ k)

Proof state:
case h_X
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g : τ → S
p p✝ : MvPolynomial σ R
n✝ : σ
a✝ : eval₂ f g ((rename k) p✝) = eval₂ f (g ∘ k) p✝
⊢ eval₂ f g ((rename k) (p✝ * X n✝)) = eval₂ f (g ∘ k) (p✝ * X n✝)

Tactic:
simp [*]

Result:
no goals

Proof state:
case h_X
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g : τ → S
p : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    eval₂ f g ((rename k) p) = eval₂ f (g ∘ k) p → eval₂ f g ((rename k) (p * X n)) = eval₂ f (g ∘ k) (p * X n)

Tactic:
intros

Result:
case h_X
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g : τ → S
p p✝ : MvPolynomial σ R
n✝ : σ
a✝ : eval₂ f g ((rename k) p✝) = eval₂ f (g ∘ k) p✝
⊢ eval₂ f g ((rename k) (p✝ * X n✝)) = eval₂ f (g ∘ k) (p✝ * X n✝)
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem Sublist.diff_right : ∀ {l₁ l₂ l₃ : List α}, l₁ <+ l₂ → l₁.diff l₃ <+ l₂.diff l₃
  | _,  _, [], h => h
  | l₁, l₂, a :: l₃, h => by simp only [diff_cons, (h.erase _).diff_right]

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List α
a : α
l₃ : List α
h : l₁ <+ l₂
⊢ l₁.diff (a :: l₃) <+ l₂.diff (a :: l₃)

Tactic:
simp only [diff_cons, (h.erase _).diff_right]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem sin_oangle_sub_left_mul_norm_of_oangle_eq_pi_div_two {x y : V}
    (h : o.oangle x y = ↑(π / 2)) : Real.Angle.sin (o.oangle (x - y) x) * ‖x - y‖ = ‖y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle (x - y) x).sin * ‖x - y‖ = ‖y‖

Tactic:
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ ((-o).oangle x (x - y)).sin * ‖x - y‖ = ‖y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ ((-o).oangle x (x - y)).sin * ‖x - y‖ = ‖y‖

Tactic:
exact (-o).sin_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two h

Result:
no goals
-- Mathlib/CategoryTheory/Generator/Basic.lean
theorem isCoseparator_unop_iff (G : Cᵒᵖ) : IsCoseparator (unop G) ↔ IsSeparator G

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : Cᵒᵖ
⊢ IsCoseparator (unop G) ↔ IsSeparator G

Tactic:
rw [IsSeparator, IsCoseparator, ← isCoseparating_unop_iff, Set.singleton_unop]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem map_take (f : α → β) :
    ∀ (L : List α) (i : Nat), (L.take i).map f = (L.map f).take i
  | [], i => by simp
  | _, 0 => by simp
  | h :: t, n + 1 => by dsimp; rw [map_take f t n]

Proof state:
α : Type u_1
β : Type u_2
f : α → β
h : α
t : List α
n : Nat
⊢ f h :: map f (take n t) = f h :: take n (map f t)

Tactic:
rw [map_take f t n]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
x✝ : List α
⊢ map f (take 0 x✝) = take 0 (map f x✝)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
i : Nat
⊢ map f (take i []) = take i (map f [])

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
h : α
t : List α
n : Nat
⊢ map f (take (n + 1) (h :: t)) = take (n + 1) (map f (h :: t))

Tactic:
dsimp

Result:
α : Type u_1
β : Type u_2
f : α → β
h : α
t : List α
n : Nat
⊢ f h :: map f (take n t) = f h :: take n (map f t)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.lean
theorem go_get (aig : AIG α) (distance : Nat) (input : AIG.RefVec aig w) (curr : Nat)
    (hcurr : curr ≤ w) (s : AIG.RefVec aig curr) :
    ∀ (idx : Nat) (hidx : idx < curr),
        (go aig input distance curr hcurr s).vec.get idx (by omega)
          =
        (s.get idx hidx).cast (by apply go_le_size)

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefVec w
curr : Nat
hcurr : curr ≤ w
s : aig.RefVec curr
idx✝ : Nat
hidx✝ : idx✝ < curr
⊢ (go aig input distance curr hcurr s).vec.get idx✝ ⋯ = (s.get idx✝ hidx✝).cast ⋯

Tactic:
apply go_get_aux

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefVec w
curr : Nat
hcurr : curr ≤ w
s : aig.RefVec curr
idx : Nat
hidx : idx < curr
⊢ idx < w

Tactic:
omega

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefVec w
curr : Nat
hcurr : curr ≤ w
s : aig.RefVec curr
⊢ ∀ (idx : Nat) (hidx : idx < curr), (go aig input distance curr hcurr s).vec.get idx ⋯ = (s.get idx hidx).cast ⋯

Tactic:
intros

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefVec w
curr : Nat
hcurr : curr ≤ w
s : aig.RefVec curr
idx✝ : Nat
hidx✝ : idx✝ < curr
⊢ (go aig input distance curr hcurr s).vec.get idx✝ ⋯ = (s.get idx✝ hidx✝).cast ⋯

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefVec w
curr : Nat
hcurr : curr ≤ w
s : aig.RefVec curr
idx : Nat
hidx : idx < curr
⊢ aig.decls.size ≤ (go aig input distance curr hcurr s).aig.decls.size

Tactic:
apply go_le_size

Result:
no goals
-- Mathlib/Data/Real/Basic.lean
theorem add_lt_add_iff_left {a b : ℝ} (c : ℝ) : c + a < c + b ↔ a < b

Proof state:
case h.h.h
y✝² y✝¹ y✝ : CauSeq ℚ abs
⊢ y✝ + y✝² < y✝ + y✝¹ ↔ y✝² < y✝¹

Tactic:
show Pos _ ↔ Pos _

Result:
case h.h.h
y✝² y✝¹ y✝ : CauSeq ℚ abs
⊢ (y✝ + y✝¹ - (y✝ + y✝²)).Pos ↔ (y✝¹ - y✝²).Pos

Proof state:
a b c : ℝ
⊢ c + a < c + b ↔ a < b

Tactic:
induction a using Real.ind_mk

Result:
case h
b c : ℝ
y✝ : CauSeq ℚ abs
⊢ c + mk y✝ < c + b ↔ mk y✝ < b

Proof state:
case h
b c : ℝ
y✝ : CauSeq ℚ abs
⊢ c + mk y✝ < c + b ↔ mk y✝ < b

Tactic:
induction b using Real.ind_mk

Result:
case h.h
c : ℝ
y✝¹ y✝ : CauSeq ℚ abs
⊢ c + mk y✝¹ < c + mk y✝ ↔ mk y✝¹ < mk y✝

Proof state:
case h.h.h
y✝² y✝¹ y✝ : CauSeq ℚ abs
⊢ (y✝ + y✝¹ - (y✝ + y✝²)).Pos ↔ (y✝¹ - y✝²).Pos

Tactic:
rw [add_sub_add_left_eq_sub]

Result:
no goals

Proof state:
case h.h.h
y✝² y✝¹ y✝ : CauSeq ℚ abs
⊢ mk y✝ + mk y✝² < mk y✝ + mk y✝¹ ↔ mk y✝² < mk y✝¹

Tactic:
simp only [mk_lt, ← mk_add]

Result:
case h.h.h
y✝² y✝¹ y✝ : CauSeq ℚ abs
⊢ y✝ + y✝² < y✝ + y✝¹ ↔ y✝² < y✝¹

Proof state:
case h.h
c : ℝ
y✝¹ y✝ : CauSeq ℚ abs
⊢ c + mk y✝¹ < c + mk y✝ ↔ mk y✝¹ < mk y✝

Tactic:
induction c using Real.ind_mk

Result:
case h.h.h
y✝² y✝¹ y✝ : CauSeq ℚ abs
⊢ mk y✝ + mk y✝² < mk y✝ + mk y✝¹ ↔ mk y✝² < mk y✝¹
-- Mathlib/Algebra/Algebra/Operations.lean
lemma mul_def : M * N = span R (M * N : Set A)

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
⊢ M * N = span R (↑M * ↑N)

Tactic:
simp [← span_mul_span]

Result:
no goals
-- Mathlib/Probability/Moments/Basic.lean
theorem IndepFun.mgf_add' {X Y : Ω → ℝ} (h_indep : IndepFun X Y μ) (hX : AEStronglyMeasurable X μ)
    (hY : AEStronglyMeasurable Y μ) : mgf (X + Y) μ t = mgf X μ t * mgf Y μ t

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : IndepFun X Y μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
A : Continuous fun x => rexp (t * x)
h'X : AEStronglyMeasurable (fun ω => rexp (t * X ω)) μ
h'Y : AEStronglyMeasurable (fun ω => rexp (t * Y ω)) μ
⊢ mgf (X + Y) μ t = mgf X μ t * mgf Y μ t

Tactic:
exact h_indep.mgf_add h'X h'Y

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : IndepFun X Y μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
⊢ Continuous fun x => rexp (t * x)

Tactic:
fun_prop

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : IndepFun X Y μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
⊢ mgf (X + Y) μ t = mgf X μ t * mgf Y μ t

Tactic:
have A : Continuous fun x : ℝ => exp (t * x) := by fun_prop

Result:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : IndepFun X Y μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
A : Continuous fun x => rexp (t * x)
⊢ mgf (X + Y) μ t = mgf X μ t * mgf Y μ t

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : IndepFun X Y μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
A : Continuous fun x => rexp (t * x)
h'X : AEStronglyMeasurable (fun ω => rexp (t * X ω)) μ
⊢ mgf (X + Y) μ t = mgf X μ t * mgf Y μ t

Tactic:
have h'Y : AEStronglyMeasurable (fun ω => exp (t * Y ω)) μ :=
  A.aestronglyMeasurable.comp_aemeasurable hY.aemeasurable

Result:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : IndepFun X Y μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
A : Continuous fun x => rexp (t * x)
h'X : AEStronglyMeasurable (fun ω => rexp (t * X ω)) μ
h'Y : AEStronglyMeasurable (fun ω => rexp (t * Y ω)) μ
⊢ mgf (X + Y) μ t = mgf X μ t * mgf Y μ t

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : IndepFun X Y μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
A : Continuous fun x => rexp (t * x)
⊢ mgf (X + Y) μ t = mgf X μ t * mgf Y μ t

Tactic:
have h'X : AEStronglyMeasurable (fun ω => exp (t * X ω)) μ :=
  A.aestronglyMeasurable.comp_aemeasurable hX.aemeasurable

Result:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : IndepFun X Y μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
A : Continuous fun x => rexp (t * x)
h'X : AEStronglyMeasurable (fun ω => rexp (t * X ω)) μ
⊢ mgf (X + Y) μ t = mgf X μ t * mgf Y μ t
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem add_ediv_of_dvd_right {a b c : Int} (H : c ∣ b) : (a + b) / c = a / c + b / c :=
  if h : c = 0 then by simp [h] else by
    let ⟨k, hk⟩ := H
    rw [hk, Int.mul_comm c k, Int.add_mul_ediv_right _ _ h,
      ← Int.zero_add (k * c), Int.add_mul_ediv_right _ _ h, Int.zero_ediv, Int.zero_add]

Proof state:
a b c : Int
H : c ∣ b
h : ¬c = 0
⊢ (a + b) / c = a / c + b / c

Tactic:
let ⟨k, hk⟩ := H

Result:
a b c : Int
H : c ∣ b
h : ¬c = 0
k : Int
hk : b = c * k
⊢ (a + b) / c = a / c + b / c

Proof state:
a b c : Int
H : c ∣ b
h : ¬c = 0
k : Int
hk : b = c * k
⊢ (a + b) / c = a / c + b / c

Tactic:
rw [hk, Int.mul_comm c k, Int.add_mul_ediv_right _ _ h,
  ← Int.zero_add (k * c), Int.add_mul_ediv_right _ _ h, Int.zero_ediv, Int.zero_add]

Result:
no goals

Proof state:
a b c : Int
H : c ∣ b
h : c = 0
⊢ (a + b) / c = a / c + b / c

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
/-- Variant of `Real.rpow_add'` that avoids having to prove `y + z = w` twice. -/
lemma rpow_of_add_eq (hx : 0 ≤ x) (hw : w ≠ 0) (h : y + z = w) : x ^ w = x ^ y * x ^ z

Proof state:
w x y z : ℝ
hx : 0 ≤ x
hw : w ≠ 0
h : y + z = w
⊢ y + z ≠ 0

Tactic:
rwa [h]

Result:
no goals

Proof state:
w x y z : ℝ
hx : 0 ≤ x
hw : w ≠ 0
h : y + z = w
⊢ x ^ w = x ^ y * x ^ z

Tactic:
rw [← h, rpow_add' hx]

Result:
w x y z : ℝ
hx : 0 ≤ x
hw : w ≠ 0
h : y + z = w
⊢ y + z ≠ 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem findSomeM?_toList [Monad m] [LawfulMonad m] (f : α → m (Option β)) (v : Vector α n) :
    v.toList.findSomeM? f = v.findSomeM? f

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
n : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
v : Vector α n
⊢ List.findSomeM? f v.toList = findSomeM? f v

Tactic:
cases v

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
n : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ List.findSomeM? f { toArray := toArray✝, size_toArray := size_toArray✝ }.toList =
    findSomeM? f { toArray := toArray✝, size_toArray := size_toArray✝ }

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
n : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ List.findSomeM? f { toArray := toArray✝, size_toArray := size_toArray✝ }.toList =
    findSomeM? f { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem real_inner_sub_sub_self (x y : F) :
    ⟪x - y, x - y⟫_ℝ = ⟪x, x⟫_ℝ - 2 * ⟪x, y⟫_ℝ + ⟪y, y⟫_ℝ

Proof state:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
this : ⟪y, x⟫_ℝ = ⟪x, y⟫_ℝ
⊢ ⟪x, x⟫_ℝ - ⟪x, y⟫_ℝ - ⟪x, y⟫_ℝ = ⟪x, x⟫_ℝ - 2 * ⟪x, y⟫_ℝ

Tactic:
ring

Result:
no goals

Proof state:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ ⟪y, x⟫_ℝ = ⟪x, y⟫_ℝ

Tactic:
rw [← inner_conj_symm]

Result:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ (starRingEnd ℝ) ⟪x, y⟫_ℝ = ⟪x, y⟫_ℝ

Proof state:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
this : ⟪y, x⟫_ℝ = ⟪x, y⟫_ℝ
⊢ ⟪x - y, x - y⟫_ℝ = ⟪x, x⟫_ℝ - 2 * ⟪x, y⟫_ℝ + ⟪y, y⟫_ℝ

Tactic:
simp only [inner_sub_sub_self, this, add_left_inj]

Result:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
this : ⟪y, x⟫_ℝ = ⟪x, y⟫_ℝ
⊢ ⟪x, x⟫_ℝ - ⟪x, y⟫_ℝ - ⟪x, y⟫_ℝ = ⟪x, x⟫_ℝ - 2 * ⟪x, y⟫_ℝ

Proof state:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ (starRingEnd ℝ) ⟪x, y⟫_ℝ = ⟪x, y⟫_ℝ

Tactic:
rfl

Result:
no goals

Proof state:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ ⟪x - y, x - y⟫_ℝ = ⟪x, x⟫_ℝ - 2 * ⟪x, y⟫_ℝ + ⟪y, y⟫_ℝ

Tactic:
have : ⟪y, x⟫_ℝ = ⟪x, y⟫_ℝ := by rw [← inner_conj_symm]; rfl

Result:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
this : ⟪y, x⟫_ℝ = ⟪x, y⟫_ℝ
⊢ ⟪x - y, x - y⟫_ℝ = ⟪x, x⟫_ℝ - 2 * ⟪x, y⟫_ℝ + ⟪y, y⟫_ℝ