harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/AddTorsor/Defs.lean
theorem vadd_vsub_eq_sub_vsub (g : G) (p q : P) : (g +ᵥ p) -ᵥ q = g - (q -ᵥ p)

Proof state:
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
g : G
p q : P
⊢ (g +ᵥ p) -ᵥ q = g - (q -ᵥ p)

Tactic:
rw [vadd_vsub_assoc, sub_eq_add_neg, neg_vsub_eq_vsub_rev]

Result:
no goals
-- Mathlib/Order/WithBot.lean
lemma lt_coe_iff : x < b ↔ ∀ a : α, x = a → a < b

Proof state:
α : Type u_1
b : α
inst✝ : LT α
x : WithBot α
⊢ x < ↑b ↔ ∀ (a : α), x = ↑a → a < b

Tactic:
simp [lt_def]

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Basic.lean
theorem prod_alternatingWord_eq_mul_pow (i i' : B) (m : ℕ) :
    π (alternatingWord i i' m) = (if Even m then 1 else s i') * (s i * s i') ^ (m / 2)

Proof state:
case pos
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
ih :
  cs.wordProd (alternatingWord i i' m) = (if Even m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 2)
hm : Even m
h₁ : ¬Even (m + 1)
⊢ cs.simple (if Even m then i' else i) *
      ((if Even m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 2)) =
    (if Even (m + 1) then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ ((m + 1) / 2)

Tactic:
have h₂ : (m + 1) / 2 = m / 2 := Nat.succ_div_of_not_dvd <| by rwa [← even_iff_two_dvd]

Result:
case pos
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
ih :
  cs.wordProd (alternatingWord i i' m) = (if Even m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 2)
hm : Even m
h₁ : ¬Even (m + 1)
h₂ : (m + 1) / 2 = m / 2
⊢ cs.simple (if Even m then i' else i) *
      ((if Even m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 2)) =
    (if Even (m + 1) then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ ((m + 1) / 2)

Proof state:
case pos
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
ih :
  cs.wordProd (alternatingWord i i' m) = (if Even m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 2)
hm : Even m
h₁ : ¬Even (m + 1)
h₂ : (m + 1) / 2 = m / 2
⊢ cs.simple (if Even m then i' else i) *
      ((if Even m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 2)) =
    (if Even (m + 1) then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ ((m + 1) / 2)

Tactic:
simp [hm, h₁, h₂]

Result:
no goals

Proof state:
case neg
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
ih :
  cs.wordProd (alternatingWord i i' m) = (if Even m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 2)
hm : ¬Even m
h₁ : Even (m + 1)
⊢ cs.simple (if Even m then i' else i) *
      ((if Even m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 2)) =
    (if Even (m + 1) then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ ((m + 1) / 2)

Tactic:
have h₂ : (m + 1) / 2 = m / 2 + 1 := Nat.succ_div_of_dvd h₁.two_dvd

Result:
case neg
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
ih :
  cs.wordProd (alternatingWord i i' m) = (if Even m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 2)
hm : ¬Even m
h₁ : Even (m + 1)
h₂ : (m + 1) / 2 = m / 2 + 1
⊢ cs.simple (if Even m then i' else i) *
      ((if Even m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 2)) =
    (if Even (m + 1) then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ ((m + 1) / 2)
-- Mathlib/Topology/Hom/ContinuousEvalConst.lean
theorem ContinuousEvalConst.of_continuous_forget {F' : Type*} [FunLike F' α X] [TopologicalSpace F']
    {f : F' → F} (hc : Continuous f) (hf : ∀ g, ⇑(f g) = g

Proof state:
F : Type u_1
α : Type u_2
X : Type u_3
inst✝⁵ : FunLike F α X
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalSpace X
inst✝² : ContinuousEvalConst F α X
F' : Type u_5
inst✝¹ : FunLike F' α X
inst✝ : TopologicalSpace F'
f : F' → F
hc : Continuous f
hf : autoParam (∀ (g : F'), ⇑(f g) = ⇑g) _auto✝
x : α
⊢ Continuous fun f => f x

Tactic:
simpa only [← hf] using (continuous_eval_const x).comp hc

Result:
no goals
-- Mathlib/Order/WithBot.lean
lemma forall_le_iff_eq_bot [NoMinOrder α] : (∀ b : α, x ≤ b) ↔ x = ⊥

Proof state:
α : Type u_1
inst✝¹ : Preorder α
x : WithBot α
inst✝ : NoMinOrder α
h : ∀ (b : α), x ≤ ↑b
y : α
⊢ x < ↑y

Tactic:
obtain ⟨w, hw⟩ := exists_lt y

Result:
case intro
α : Type u_1
inst✝¹ : Preorder α
x : WithBot α
inst✝ : NoMinOrder α
h : ∀ (b : α), x ≤ ↑b
y w : α
hw : w < y
⊢ x < ↑y

Proof state:
α : Type u_1
inst✝¹ : Preorder α
x : WithBot α
inst✝ : NoMinOrder α
⊢ (∀ (b : α), x ≤ ↑b) ↔ x = ⊥

Tactic:
refine ⟨fun h ↦ forall_lt_iff_eq_bot.1 fun y ↦ ?_, by simp +contextual⟩

Result:
α : Type u_1
inst✝¹ : Preorder α
x : WithBot α
inst✝ : NoMinOrder α
h : ∀ (b : α), x ≤ ↑b
y : α
⊢ x < ↑y

Proof state:
α : Type u_1
inst✝¹ : Preorder α
x : WithBot α
inst✝ : NoMinOrder α
⊢ x = ⊥ → ∀ (b : α), x ≤ ↑b

Tactic:
simp +contextual

Result:
no goals

Proof state:
case intro
α : Type u_1
inst✝¹ : Preorder α
x : WithBot α
inst✝ : NoMinOrder α
h : ∀ (b : α), x ≤ ↑b
y w : α
hw : w < y
⊢ x < ↑y

Tactic:
exact (h w).trans_lt (coe_lt_coe.2 hw)

Result:
no goals
-- Mathlib/Algebra/Ring/Basic.lean
lemma div_neg_eq_neg_div (a b : R) : b / -a = -(b / a) :=
  calc
    b / -a = b * (1 / -a)

Proof state:
R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
a b : R
⊢ -(b * (1 / a)) = -(b / a)

Tactic:
rw [mul_one_div]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
a b : R
⊢ b * (1 / -a) = b * -(1 / a)

Tactic:
rw [one_div_neg_eq_neg_one_div]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
a b : R
⊢ b / -a = b * (1 / -a)

Tactic:
rw [← inv_eq_one_div, division_def]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
a b : R
⊢ b * -(1 / a) = -(b * (1 / a))

Tactic:
rw [neg_mul_eq_mul_neg]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Dickson.lean
theorem map_dickson (f : R →+* S) : ∀ n : ℕ, map f (dickson k a n) = dickson k (f a) n
  | 0 => by
    simp_rw [dickson_zero, Polynomial.map_sub, Polynomial.map_natCast, Polynomial.map_ofNat]
  | 1 => by simp only [dickson_one, map_X]
  | n + 2 => by
    simp only [dickson_add_two, Polynomial.map_sub, Polynomial.map_mul, map_X, map_C]
    rw [map_dickson f n, map_dickson f (n + 1)]

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
f : R →+* S
⊢ map f (dickson k a 0) = dickson k (f a) 0

Tactic:
simp_rw [dickson_zero, Polynomial.map_sub, Polynomial.map_natCast, Polynomial.map_ofNat]

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
f : R →+* S
n : ℕ
⊢ X * map f (dickson k a (n + 1)) - C (f a) * map f (dickson k a n) =
    X * dickson k (f a) (n + 1) - C (f a) * dickson k (f a) n

Tactic:
rw [map_dickson f n, map_dickson f (n + 1)]

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
f : R →+* S
⊢ map f (dickson k a 1) = dickson k (f a) 1

Tactic:
simp only [dickson_one, map_X]

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
f : R →+* S
n : ℕ
⊢ map f (dickson k a (n + 2)) = dickson k (f a) (n + 2)

Tactic:
simp only [dickson_add_two, Polynomial.map_sub, Polynomial.map_mul, map_X, map_C]

Result:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
f : R →+* S
n : ℕ
⊢ X * map f (dickson k a (n + 1)) - C (f a) * map f (dickson k a n) =
    X * dickson k (f a) (n + 1) - C (f a) * dickson k (f a) n
-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem leadingCoeff_pow_of_pow_leadingCoeff_ne_zero {f : MvPolynomial σ R} {n : ℕ}
    (hf : m.leadingCoeff f ^ n ≠ 0) :
    m.leadingCoeff (f ^ n) = m.leadingCoeff f ^ n

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
n : ℕ
hf : m.leadingCoeff f ^ n ≠ 0
⊢ m.leadingCoeff (f ^ n) = m.leadingCoeff f ^ n

Tactic:
rw [leadingCoeff, degree_pow_of_pow_leadingCoeff_ne_zero hf, coeff_pow_nsmul_degree]

Result:
no goals
-- Mathlib/Topology/Algebra/Group/Basic.lean
@[to_additive]
lemma IsClosed.mul_closure_one_eq {F : Set G} (hF : IsClosed F) :
    F * (closure {1} : Set G) = F

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
F : Set G
hF : IsClosed F
⊢ F * closure {1} = F

Tactic:
refine Subset.antisymm ?_ (subset_mul_closure_one F)

Result:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
F : Set G
hF : IsClosed F
⊢ F * closure {1} ⊆ F

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
F : Set G
hF : IsClosed F
⊢ F * closure {1} ⊆ F

Tactic:
calc
F * (closure {1} : Set G) = closure F * closure ({1} : Set G) := by rw [hF.closure_eq]
_ ⊆ closure (F * ({1} : Set G)) := smul_set_closure_subset _ _
_ = F := by simp [hF.closure_eq]

Result:
no goals

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
F : Set G
hF : IsClosed F
⊢ F * closure {1} = closure F * closure {1}

Tactic:
rw [hF.closure_eq]

Result:
no goals

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
F : Set G
hF : IsClosed F
⊢ closure (F * {1}) = F

Tactic:
simp [hF.closure_eq]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Basic.lean
theorem integral_neg : integral I l (-f) vol = -integral I l f vol

Proof state:
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
⊢ integral I l (-f) vol = -integral I l f vol

Tactic:
classical
exact if h : Integrable I l f vol then h.hasIntegral.neg.integral_eq
else by rw [integral, integral, dif_neg h, dif_neg (mt Integrable.of_neg h), neg_zero]

Result:
no goals

Proof state:
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
h : ¬Integrable I l f vol
⊢ integral I l (-f) vol = -integral I l f vol

Tactic:
rw [integral, integral, dif_neg h, dif_neg (mt Integrable.of_neg h), neg_zero]

Result:
no goals

Proof state:
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
⊢ integral I l (-f) vol = -integral I l f vol

Tactic:
exact if h : Integrable I l f vol then h.hasIntegral.neg.integral_eq
else by rw [integral, integral, dif_neg h, dif_neg (mt Integrable.of_neg h), neg_zero]

Result:
no goals
-- Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
theorem _root_.List.stronglyMeasurable_prod (l : List (α → M))
    (hl : ∀ f ∈ l, StronglyMeasurable f) :
    StronglyMeasurable fun x => (l.map fun f : α → M => f x).prod

Proof state:
α : Type u_1
M : Type u_5
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
m : MeasurableSpace α
l : List (α → M)
hl : ∀ f ∈ l, StronglyMeasurable f
⊢ StronglyMeasurable fun x => (List.map (fun f => f x) l).prod

Tactic:
simpa only [← Pi.list_prod_apply] using l.stronglyMeasurable_prod' hl

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem Dense.inter_of_isOpen_left (hs : Dense s) (ht : Dense t) (hso : IsOpen s) :
    Dense (s ∩ t) := fun x =>
  closure_minimal hso.inter_closure isClosed_closure <| by simp [hs.closure_eq, ht.closure_eq]

Proof state:
X : Type u
s t : Set X
inst✝ : TopologicalSpace X
hs : Dense s
ht : Dense t
hso : IsOpen s
x : X
⊢ x ∈ closure (s ∩ closure t)

Tactic:
simp [hs.closure_eq, ht.closure_eq]

Result:
no goals
-- Mathlib/Analysis/Analytic/Within.lean
/-- `f` is analytic within `s` at `x` iff some local extension of `f` is analytic at `x` -/
lemma analyticWithinAt_iff_exists_analyticAt [CompleteSpace F] {f : E → F} {s : Set E} {x : E} :
    AnalyticWithinAt 𝕜 f s x ↔
      ∃ g, f =ᶠ[𝓝[insert x s] x] g ∧ AnalyticAt 𝕜 g x

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
s : Set E
x : E
⊢ (∃ p g, f =ᶠ[𝓝[insert x s] x] g ∧ HasFPowerSeriesAt g p x) ↔
    ∃ g, f =ᶠ[𝓝[insert x s] x] g ∧ ∃ p, HasFPowerSeriesAt g p x

Tactic:
tauto

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
s : Set E
x : E
⊢ AnalyticWithinAt 𝕜 f s x ↔ ∃ g, f =ᶠ[𝓝[insert x s] x] g ∧ AnalyticAt 𝕜 g x

Tactic:
simp only [AnalyticWithinAt, AnalyticAt, hasFPowerSeriesWithinAt_iff_exists_hasFPowerSeriesAt]

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
s : Set E
x : E
⊢ (∃ p g, f =ᶠ[𝓝[insert x s] x] g ∧ HasFPowerSeriesAt g p x) ↔
    ∃ g, f =ᶠ[𝓝[insert x s] x] g ∧ ∃ p, HasFPowerSeriesAt g p x
-- Mathlib/MeasureTheory/Measure/FiniteMeasureProd.lean
@[simp] lemma zero_prod : (0 : FiniteMeasure α).prod ν = 0

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
ν : FiniteMeasure β
⊢ prod 0 ν = 0

Tactic:
rw [← mass_zero_iff, mass_prod, zero_mass, zero_mul]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Smeval.lean
theorem leval_coe_eq_smeval {R : Type*} [Semiring R] (r : R) :
    ⇑(leval r) = fun p => p.smeval r

Proof state:
R : Type u_3
inst✝ : Semiring R
r : R
x✝ : R[X]
⊢ (leval r) x✝ = x✝.smeval r

Tactic:
rw [leval_apply, smeval_def, eval_eq_sum]

Result:
R : Type u_3
inst✝ : Semiring R
r : R
x✝ : R[X]
⊢ (x✝.sum fun e a => a * r ^ e) = x✝.sum (smul_pow r)

Proof state:
R : Type u_3
inst✝ : Semiring R
r : R
x✝ : R[X]
⊢ (x✝.sum fun e a => a * r ^ e) = x✝.sum (smul_pow r)

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_3
inst✝ : Semiring R
r : R
⊢ ⇑(leval r) = fun p => p.smeval r

Tactic:
rw [funext_iff]

Result:
R : Type u_3
inst✝ : Semiring R
r : R
⊢ ∀ (x : R[X]), (leval r) x = x.smeval r

Proof state:
R : Type u_3
inst✝ : Semiring R
r : R
⊢ ∀ (x : R[X]), (leval r) x = x.smeval r

Tactic:
intro

Result:
R : Type u_3
inst✝ : Semiring R
r : R
x✝ : R[X]
⊢ (leval r) x✝ = x✝.smeval r
-- Mathlib/Data/QPF/Multivariate/Constructions/Fix.lean
theorem recF_eq {α : TypeVec n} {β : Type u} (g : F (α.append1 β) → β) (a : q.P.A)
    (f' : q.P.drop.B a ⟹ α) (f : q.P.last.B a → q.P.W α) :
    recF g (q.P.wMk a f' f) = g (abs ⟨a, splitFun f' (recF g ∘ f)⟩)

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ recF g ((P F).wMk a f' f) = g (abs ⟨a, splitFun f' (recF g ∘ f)⟩)

Tactic:
rw [recF, MvPFunctor.wRec_eq]

Result:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ g (abs ⟨a, splitFun f' fun i => (P F).wRec (fun a f' _f rec => g (abs ⟨a, splitFun f' rec⟩)) (f i)⟩) =
    g (abs ⟨a, splitFun f' (((P F).wRec fun a f' _f rec => g (abs ⟨a, splitFun f' rec⟩)) ∘ f)⟩)

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ g (abs ⟨a, splitFun f' fun i => (P F).wRec (fun a f' _f rec => g (abs ⟨a, splitFun f' rec⟩)) (f i)⟩) =
    g (abs ⟨a, splitFun f' (((P F).wRec fun a f' _f rec => g (abs ⟨a, splitFun f' rec⟩)) ∘ f)⟩)

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCast_cons [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k}
    (h : containsKey a (⟨k, v⟩ :: l)) :
    getValueCast a (⟨k, v⟩ :: l) h =
      if h' : k == a then
        cast (congrArg β (eq_of_beq h')) v
      else
        getValueCast a l (containsKey_of_containsKey_cons (k := k) h (Bool.eq_false_iff.2 h'))

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k a : α
v : β k
h : containsKey a (⟨k, v⟩ :: l) = true
⊢ (if h : (k == a) = true then some (cast ⋯ v) else getValueCast? a l).get ⋯ =
    if h' : (k == a) = true then cast ⋯ v else getValueCast a l ⋯

Tactic:
split <;> simp [getValueCast]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k a : α
v : β k
h : containsKey a (⟨k, v⟩ :: l) = true
⊢ getValueCast a (⟨k, v⟩ :: l) h = if h' : (k == a) = true then cast ⋯ v else getValueCast a l ⋯

Tactic:
rw [getValueCast, Option.get_congr getValueCast?_cons]

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k a : α
v : β k
h : containsKey a (⟨k, v⟩ :: l) = true
⊢ (if h : (k == a) = true then some (cast ⋯ v) else getValueCast? a l).get ⋯ =
    if h' : (k == a) = true then cast ⋯ v else getValueCast a l ⋯
-- Mathlib/Algebra/Homology/Opposite.lean
@[reassoc (attr := simp)]
lemma opcyclesOpIso_hom_toCycles_op :
    (K.opcyclesOpIso i).hom ≫ (K.toCycles j i).op = K.op.fromOpcycles i j

Proof state:
ι : Type u_1
V : Type u_2
inst✝² : Category.{u_3, u_2} V
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms V
K : HomologicalComplex V c
i : ι
inst✝ : K.HasHomology i
j : ι
⊢ (K.opcyclesOpIso i).hom ≫ (K.toCycles j i).op = K.op.fromOpcycles i j

Tactic:
by_cases hij : c.Rel j i

Result:
case pos
ι : Type u_1
V : Type u_2
inst✝² : Category.{u_3, u_2} V
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms V
K : HomologicalComplex V c
i : ι
inst✝ : K.HasHomology i
j : ι
hij : c.Rel j i
⊢ (K.opcyclesOpIso i).hom ≫ (K.toCycles j i).op = K.op.fromOpcycles i j

case neg
ι : Type u_1
V : Type u_2
inst✝² : Category.{u_3, u_2} V
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms V
K : HomologicalComplex V c
i : ι
inst✝ : K.HasHomology i
j : ι
hij : ¬c.Rel j i
⊢ (K.opcyclesOpIso i).hom ≫ (K.toCycles j i).op = K.op.fromOpcycles i j

Proof state:
case pos
ι : Type u_1
V : Type u_2
inst✝² : Category.{u_3, u_2} V
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms V
K : HomologicalComplex V c
i : ι
inst✝ : K.HasHomology i
hij : c.Rel (c.prev i) i
⊢ (K.opcyclesOpIso i).hom ≫ (K.toCycles (c.prev i) i).op = K.op.fromOpcycles i (c.prev i)

Tactic:
exact (K.sc i).opcyclesOpIso_hom_toCycles_op

Result:
no goals

Proof state:
case neg
ι : Type u_1
V : Type u_2
inst✝² : Category.{u_3, u_2} V
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms V
K : HomologicalComplex V c
i : ι
inst✝ : K.HasHomology i
j : ι
hij : ¬c.Rel j i
⊢ (K.opcyclesOpIso i).hom ≫ (K.toCycles j i).op = K.op.fromOpcycles i j

Tactic:
rw [K.toCycles_eq_zero hij, K.op.fromOpcycles_eq_zero hij, op_zero, comp_zero]

Result:
no goals

Proof state:
case pos
ι : Type u_1
V : Type u_2
inst✝² : Category.{u_3, u_2} V
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms V
K : HomologicalComplex V c
i : ι
inst✝ : K.HasHomology i
j : ι
hij : c.Rel j i
⊢ (K.opcyclesOpIso i).hom ≫ (K.toCycles j i).op = K.op.fromOpcycles i j

Tactic:
obtain rfl := c.prev_eq' hij

Result:
case pos
ι : Type u_1
V : Type u_2
inst✝² : Category.{u_3, u_2} V
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms V
K : HomologicalComplex V c
i : ι
inst✝ : K.HasHomology i
hij : c.Rel (c.prev i) i
⊢ (K.opcyclesOpIso i).hom ≫ (K.toCycles (c.prev i) i).op = K.op.fromOpcycles i (c.prev i)
-- Mathlib/CategoryTheory/Subobject/FactorThru.lean
theorem mk_factors_self (f : X ⟶ Y) [Mono f] : (mk f).Factors f :=
  ⟨𝟙 _, by simp⟩

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
⊢ 𝟙 X ≫ (MonoOver.mk' f).arrow = f

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Module/CharacterModule.lean
@[simp]
lemma dual_zero : dual (0 : A →ₗ[R] B) = 0

Proof state:
R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
B : Type uB
inst✝² : AddCommGroup B
inst✝¹ : Module R A
inst✝ : Module R B
⊢ dual 0 = 0

Tactic:
ext f

Result:
case h.h
R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
B : Type uB
inst✝² : AddCommGroup B
inst✝¹ : Module R A
inst✝ : Module R B
f : CharacterModule B
x✝ : A
⊢ ((dual 0) f) x✝ = (0 f) x✝

Proof state:
case h.h
R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
B : Type uB
inst✝² : AddCommGroup B
inst✝¹ : Module R A
inst✝ : Module R B
f : CharacterModule B
x✝ : A
⊢ ((dual 0) f) x✝ = (0 f) x✝

Tactic:
exact map_zero f

Result:
no goals
-- Mathlib/Data/DFinsupp/Defs.lean
theorem update_eq_single_add_erase {β : ι → Type*} [∀ i, AddZeroClass (β i)] (f : Π₀ i, β i)
    (i : ι) (b : β i) : f.update i b = single i b + f.erase i

Proof state:
ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
⊢ f.update i b = single i b + erase i f

Tactic:
ext j

Result:
case h
ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
j : ι
⊢ (f.update i b) j = (single i b + erase i f) j

Proof state:
case h.inr
ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
j : ι
h : i ≠ j
⊢ (f.update i b) j = (single i b + erase i f) j

Tactic:
simp [Function.update_of_ne h.symm, h, erase_ne, h.symm]

Result:
no goals

Proof state:
case h
ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
j : ι
⊢ (f.update i b) j = (single i b + erase i f) j

Tactic:
rcases eq_or_ne i j with (rfl | h)

Result:
case h.inl
ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
⊢ (f.update i b) i = (single i b + erase i f) i

case h.inr
ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
j : ι
h : i ≠ j
⊢ (f.update i b) j = (single i b + erase i f) j

Proof state:
case h.inl
ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
⊢ (f.update i b) i = (single i b + erase i f) i

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem_swap_right (a : Array α) {i j : Nat} {hi hj} :
    (a.swap i j hi hj)[j]'(by simpa using hj) = a[i]

Proof state:
α : Type u_1
a : Array α
i j : Nat
hi : i < a.size
hj : j < a.size
⊢ (a.swap i j hi hj)[j] = a[i]

Tactic:
simp [swap_def, getElem_set]

Result:
no goals

Proof state:
α : Type ?u.517941
a : Array α
i j : Nat
hi : i < a.size
hj : j < a.size
⊢ j < (a.swap i j hi hj).size

Tactic:
simpa using hj

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/PiL2.lean
theorem sum_repr (b : OrthonormalBasis ι 𝕜 E) (x : E) : ∑ i, b.repr x i • b i = x

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
⊢ ∑ x_1 : ι, (b.toBasis.repr x) x_1 • b.toBasis x_1 = x

Tactic:
exact b.toBasis.sum_repr x

Result:
no goals

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
⊢ ∑ i : ι, b.repr x i • b i = x

Tactic:
simp_rw [← b.coe_toBasis_repr_apply, ← b.coe_toBasis]

Result:
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
⊢ ∑ x_1 : ι, (b.toBasis.repr x) x_1 • b.toBasis x_1 = x