harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean
theorem prime_pow_le_iff_le_bcount [DecidableEq (Associates α)] {m p : Associates α}
    (h₁ : m ≠ 0) (h₂ : Irreducible p) {k : ℕ} : p ^ k ≤ m ↔ k ≤ bcount ⟨p, h₂⟩ m.factors

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : DecidableEq (Associates α)
m p : Associates α
h₁ : m ≠ 0
h₂ : Irreducible p
k : ℕ
⊢ p ^ k ≤ m ↔ k ≤ bcount ⟨p, h₂⟩ m.factors

Tactic:
rcases Associates.exists_non_zero_rep h₁ with ⟨m, hm, rfl⟩

Result:
case intro.intro
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : DecidableEq (Associates α)
p : Associates α
h₂ : Irreducible p
k : ℕ
m : α
hm : m ≠ 0
h₁ : Associates.mk m ≠ 0
⊢ p ^ k ≤ Associates.mk m ↔ k ≤ bcount ⟨p, h₂⟩ (Associates.mk m).factors

Proof state:
case intro.intro
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : DecidableEq (Associates α)
p : Associates α
h₂ : Irreducible p
k : ℕ
m : α
hm : m ≠ 0
h₁ : Associates.mk m ≠ 0
⊢ p ^ k ≤ Associates.mk m ↔ k ≤ bcount ⟨p, h₂⟩ (Associates.mk m).factors

Tactic:
have := nontrivial_of_ne _ _ hm

Result:
case intro.intro
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : DecidableEq (Associates α)
p : Associates α
h₂ : Irreducible p
k : ℕ
m : α
hm : m ≠ 0
h₁ : Associates.mk m ≠ 0
this : Nontrivial α
⊢ p ^ k ≤ Associates.mk m ↔ k ≤ bcount ⟨p, h₂⟩ (Associates.mk m).factors

Proof state:
case intro.intro
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : DecidableEq (Associates α)
p : Associates α
h₂ : Irreducible p
k : ℕ
m : α
hm : m ≠ 0
h₁ : Associates.mk m ≠ 0
this : Nontrivial α
⊢ p ^ k ≤ Associates.mk m ↔ k ≤ bcount ⟨p, h₂⟩ (Associates.mk m).factors

Tactic:
rw [bcount.eq_def, factors_mk, Multiset.le_count_iff_replicate_le, ← factors_le,
  factors_prime_pow, factors_mk, WithTop.coe_le_coe] <;> assumption

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Convolution.lean
lemma convolution_def {R : Type*} [Semiring R] (f g : ℕ → R) :
    f ⍟ g = fun n ↦ ∑ p ∈ n.divisorsAntidiagonal, f p.1 * g p.2

Proof state:
R : Type u_1
inst✝ : Semiring R
f g : ℕ → R
n : ℕ
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
⊢ (if p.2 = 0 then 0 else if p.1 = 0 then 0 else f p.1 * g p.2) = f p.1 * g p.2

Tactic:
simp [ne_zero_of_mem_divisorsAntidiagonal hp]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
f g : ℕ → R
⊢ f ⍟ g = fun n => ∑ p ∈ n.divisorsAntidiagonal, f p.1 * g p.2

Tactic:
ext n

Result:
case h
R : Type u_1
inst✝ : Semiring R
f g : ℕ → R
n : ℕ
⊢ (f ⍟ g) n = ∑ p ∈ n.divisorsAntidiagonal, f p.1 * g p.2

Proof state:
case h
R : Type u_1
inst✝ : Semiring R
f g : ℕ → R
n : ℕ
⊢ (f ⍟ g) n = ∑ p ∈ n.divisorsAntidiagonal, f p.1 * g p.2

Tactic:
simpa [convolution, toArithmeticFunction] using
  Finset.sum_congr rfl fun p hp ↦ by simp [ne_zero_of_mem_divisorsAntidiagonal hp]

Result:
no goals
-- Mathlib/Algebra/Group/NatPowAssoc.lean
theorem npow_mul' (x : M) (m n : ℕ) : x ^ (m * n) = (x ^ n) ^ m

Proof state:
M : Type u_1
inst✝² : MulOneClass M
inst✝¹ : Pow M ℕ
inst✝ : NatPowAssoc M
x : M
m n : ℕ
⊢ x ^ (m * n) = (x ^ n) ^ m

Tactic:
rw [mul_comm]

Result:
M : Type u_1
inst✝² : MulOneClass M
inst✝¹ : Pow M ℕ
inst✝ : NatPowAssoc M
x : M
m n : ℕ
⊢ x ^ (n * m) = (x ^ n) ^ m

Proof state:
M : Type u_1
inst✝² : MulOneClass M
inst✝¹ : Pow M ℕ
inst✝ : NatPowAssoc M
x : M
m n : ℕ
⊢ x ^ (n * m) = (x ^ n) ^ m

Tactic:
exact npow_mul x n m

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem tan_sq_div_one_add_tan_sq {x : ℂ} (hx : cos x ≠ 0) :
    tan x ^ 2 / (1 + tan x ^ 2) = sin x ^ 2

Proof state:
x : ℂ
hx : cos x ≠ 0
⊢ tan x ^ 2 / (1 + tan x ^ 2) = sin x ^ 2

Tactic:
simp only [← tan_mul_cos hx, mul_pow, ← inv_one_add_tan_sq hx, div_eq_mul_inv, one_mul]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Content.lean
theorem sup_disjoint (K₁ K₂ : Compacts G) (h : Disjoint (K₁ : Set G) K₂)
    (h₁ : IsClosed (K₁ : Set G)) (h₂ : IsClosed (K₂ : Set G)) :
    μ (K₁ ⊔ K₂) = μ K₁ + μ K₂

Proof state:
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
K₁ K₂ : Compacts G
h : Disjoint ↑K₁ ↑K₂
h₁ : IsClosed ↑K₁
h₂ : IsClosed ↑K₂
⊢ μ (K₁ ⊔ K₂) = μ K₁ + μ K₂

Tactic:
simpa [toNNReal_eq_toNNReal_iff, ← toNNReal_add] using μ.sup_disjoint' _ _ h h₁ h₂

Result:
no goals
-- Mathlib/Analysis/Convex/Star.lean
theorem StarConvex.preimage_add_right (hs : StarConvex 𝕜 (z + x) s) :
    StarConvex 𝕜 x ((fun x => z + x) ⁻¹' s)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x z : E
s : Set E
hs : StarConvex 𝕜 (z + x) s
⊢ StarConvex 𝕜 x ((fun x => z + x) ⁻¹' s)

Tactic:
intro y hy a b ha hb hab

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x z : E
s : Set E
hs : StarConvex 𝕜 (z + x) s
y : E
hy : y ∈ (fun x => z + x) ⁻¹' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ (fun x => z + x) ⁻¹' s

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x z : E
s : Set E
hs : StarConvex 𝕜 (z + x) s
y : E
hy : y ∈ (fun x => z + x) ⁻¹' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h : a • (z + x) + b • (fun x => z + x) y ∈ s
⊢ a • x + b • y ∈ (fun x => z + x) ⁻¹' s

Tactic:
rwa [smul_add, smul_add, add_add_add_comm, ← add_smul, hab, one_smul] at h

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x z : E
s : Set E
hs : StarConvex 𝕜 (z + x) s
y : E
hy : y ∈ (fun x => z + x) ⁻¹' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ (fun x => z + x) ⁻¹' s

Tactic:
have h := hs hy ha hb hab

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x z : E
s : Set E
hs : StarConvex 𝕜 (z + x) s
y : E
hy : y ∈ (fun x => z + x) ⁻¹' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h : a • (z + x) + b • (fun x => z + x) y ∈ s
⊢ a • x + b • y ∈ (fun x => z + x) ⁻¹' s
-- Mathlib/Data/Matroid/Basic.lean
theorem isBasis'_iff_isBasis_inter_ground : M.IsBasis' I X ↔ M.IsBasis I (X ∩ M.E)

Proof state:
α : Type u_1
M : Matroid α
I X : Set α
⊢ M.IsBasis' I X ↔ M.IsBasis I (X ∩ M.E)

Tactic:
rw [IsBasis', IsBasis, and_iff_left inter_subset_right, maximal_iff_maximal_of_imp_of_forall]

Result:
case hPQ
α : Type u_1
M : Matroid α
I X : Set α
⊢ ∀ ⦃x : Set α⦄, M.Indep x ∧ x ⊆ X ∩ M.E → M.Indep x ∧ x ⊆ X

case h
α : Type u_1
M : Matroid α
I X : Set α
⊢ ∀ ⦃x : Set α⦄, M.Indep x ∧ x ⊆ X → ∃ y, x ≤ y ∧ M.Indep y ∧ y ⊆ X ∩ M.E

Proof state:
case hPQ
α : Type u_1
M : Matroid α
I X : Set α
⊢ ∀ ⦃x : Set α⦄, M.Indep x ∧ x ⊆ X ∩ M.E → M.Indep x ∧ x ⊆ X

Tactic:
exact fun I hI ↦ ⟨hI.1, hI.2.trans inter_subset_left⟩

Result:
no goals

Proof state:
case h
α : Type u_1
M : Matroid α
I X : Set α
⊢ ∀ ⦃x : Set α⦄, M.Indep x ∧ x ⊆ X → ∃ y, x ≤ y ∧ M.Indep y ∧ y ⊆ X ∩ M.E

Tactic:
exact fun I hI ↦ ⟨I, rfl.le, hI.1, subset_inter hI.2 hI.1.subset_ground⟩

Result:
no goals
-- Mathlib/Analysis/Convex/Combination.lean
theorem Finset.centerMass_segment' (s : Finset ι) (t : Finset ι') (ws : ι → R) (zs : ι → E)
    (wt : ι' → R) (zt : ι' → E) (hws : ∑ i ∈ s, ws i = 1) (hwt : ∑ i ∈ t, wt i = 1) (a b : R)
    (hab : a + b = 1) : a • s.centerMass ws zs + b • t.centerMass wt zt = (s.disjSum t).centerMass
    (Sum.elim (fun i => a * ws i) fun j => b * wt j) (Sum.elim zs zt)

Proof state:
case hw
R : Type u_1
E : Type u_3
ι : Type u_5
ι' : Type u_6
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset ι
t : Finset ι'
ws : ι → R
zs : ι → E
wt : ι' → R
zt : ι' → E
hws : ∑ i ∈ s, ws i = 1
hwt : ∑ i ∈ t, wt i = 1
a b : R
hab : a + b = 1
⊢ ∑ i ∈ s.disjSum t, Sum.elim (fun i => a * ws i) (fun j => b * wt j) i = 1

Tactic:
rw [sum_sumElim, ← mul_sum, ← mul_sum, hws, hwt, mul_one, mul_one, hab]

Result:
no goals

Proof state:
R : Type u_1
E : Type u_3
ι : Type u_5
ι' : Type u_6
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset ι
t : Finset ι'
ws : ι → R
zs : ι → E
wt : ι' → R
zt : ι' → E
hws : ∑ i ∈ s, ws i = 1
hwt : ∑ i ∈ t, wt i = 1
a b : R
hab : a + b = 1
⊢ ∑ x ∈ s.disjSum t, Sum.elim (fun x => a • ws x • zs x) (fun x => b • wt x • zt x) x =
    ∑ i ∈ s.disjSum t, Sum.elim (fun i => a * ws i) (fun j => b * wt j) i • Sum.elim zs zt i

Tactic:
congr with ⟨⟩ <;> simp only [Sum.elim_inl, Sum.elim_inr, mul_smul]

Result:
no goals

Proof state:
R : Type u_1
E : Type u_3
ι : Type u_5
ι' : Type u_6
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset ι
t : Finset ι'
ws : ι → R
zs : ι → E
wt : ι' → R
zt : ι' → E
hws : ∑ i ∈ s, ws i = 1
hwt : ∑ i ∈ t, wt i = 1
a b : R
hab : a + b = 1
⊢ a • s.centerMass ws zs + b • t.centerMass wt zt =
    (s.disjSum t).centerMass (Sum.elim (fun i => a * ws i) fun j => b * wt j) (Sum.elim zs zt)

Tactic:
rw [s.centerMass_eq_of_sum_1 _ hws, t.centerMass_eq_of_sum_1 _ hwt, smul_sum, smul_sum, ←
  Finset.sum_sumElim, Finset.centerMass_eq_of_sum_1]

Result:
R : Type u_1
E : Type u_3
ι : Type u_5
ι' : Type u_6
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset ι
t : Finset ι'
ws : ι → R
zs : ι → E
wt : ι' → R
zt : ι' → E
hws : ∑ i ∈ s, ws i = 1
hwt : ∑ i ∈ t, wt i = 1
a b : R
hab : a + b = 1
⊢ ∑ x ∈ s.disjSum t, Sum.elim (fun x => a • ws x • zs x) (fun x => b • wt x • zt x) x =
    ∑ i ∈ s.disjSum t, Sum.elim (fun i => a * ws i) (fun j => b * wt j) i • Sum.elim zs zt i

case hw
R : Type u_1
E : Type u_3
ι : Type u_5
ι' : Type u_6
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset ι
t : Finset ι'
ws : ι → R
zs : ι → E
wt : ι' → R
zt : ι' → E
hws : ∑ i ∈ s, ws i = 1
hwt : ∑ i ∈ t, wt i = 1
a b : R
hab : a + b = 1
⊢ ∑ i ∈ s.disjSum t, Sum.elim (fun i => a * ws i) (fun j => b * wt j) i = 1
-- Mathlib/CategoryTheory/ChosenFiniteProducts.lean
theorem monoidal_of_preservesFiniteProducts (α : F ⟶ G) :
    NatTrans.IsMonoidal α where
  unit := (cancel_mono (Functor.Monoidal.εIso _).inv).1 (toUnit_unique _ _)
  tensor {X Y}

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ChosenFiniteProducts C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : ChosenFiniteProducts D
F G : C ⥤ D
inst✝¹ : Limits.PreservesFiniteProducts F
inst✝ : Limits.PreservesFiniteProducts G
α : F ⟶ G
X Y : C
⊢ Functor.LaxMonoidal.μ F X Y ≫ α.app (X ⊗ Y) = (α.app X ⊗ α.app Y) ≫ Functor.LaxMonoidal.μ G X Y

Tactic:
rw [← cancel_mono (Functor.Monoidal.μIso _ _ _).inv]

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ChosenFiniteProducts C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : ChosenFiniteProducts D
F G : C ⥤ D
inst✝¹ : Limits.PreservesFiniteProducts F
inst✝ : Limits.PreservesFiniteProducts G
α : F ⟶ G
X Y : C
⊢ (Functor.LaxMonoidal.μ F X Y ≫ α.app (X ⊗ Y)) ≫ (Functor.Monoidal.μIso G X Y).inv =
    ((α.app X ⊗ α.app Y) ≫ Functor.LaxMonoidal.μ G X Y) ≫ (Functor.Monoidal.μIso G X Y).inv

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ChosenFiniteProducts C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : ChosenFiniteProducts D
F G : C ⥤ D
inst✝¹ : Limits.PreservesFiniteProducts F
inst✝ : Limits.PreservesFiniteProducts G
α : F ⟶ G
X Y : C
⊢ (Functor.Monoidal.μIso F X Y).inv ≫
      (Functor.LaxMonoidal.μ F X Y ≫ α.app (X ⊗ Y)) ≫ (Functor.Monoidal.μIso G X Y).inv =
    (Functor.Monoidal.μIso F X Y).inv ≫
      ((α.app X ⊗ α.app Y) ≫ Functor.LaxMonoidal.μ G X Y) ≫ (Functor.Monoidal.μIso G X Y).inv

Tactic:
apply ChosenFiniteProducts.hom_ext <;> simp

Result:
no goals

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ChosenFiniteProducts C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : ChosenFiniteProducts D
F G : C ⥤ D
inst✝¹ : Limits.PreservesFiniteProducts F
inst✝ : Limits.PreservesFiniteProducts G
α : F ⟶ G
X Y : C
⊢ (Functor.LaxMonoidal.μ F X Y ≫ α.app (X ⊗ Y)) ≫ (Functor.Monoidal.μIso G X Y).inv =
    ((α.app X ⊗ α.app Y) ≫ Functor.LaxMonoidal.μ G X Y) ≫ (Functor.Monoidal.μIso G X Y).inv

Tactic:
rw [← cancel_epi (Functor.Monoidal.μIso _ _ _).inv]

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ChosenFiniteProducts C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : ChosenFiniteProducts D
F G : C ⥤ D
inst✝¹ : Limits.PreservesFiniteProducts F
inst✝ : Limits.PreservesFiniteProducts G
α : F ⟶ G
X Y : C
⊢ (Functor.Monoidal.μIso F X Y).inv ≫
      (Functor.LaxMonoidal.μ F X Y ≫ α.app (X ⊗ Y)) ≫ (Functor.Monoidal.μIso G X Y).inv =
    (Functor.Monoidal.μIso F X Y).inv ≫
      ((α.app X ⊗ α.app Y) ≫ Functor.LaxMonoidal.μ G X Y) ≫ (Functor.Monoidal.μIso G X Y).inv
-- Mathlib/Analysis/InnerProductSpace/Orthogonal.lean
theorem isClosed_orthogonal : IsClosed (Kᗮ : Set E)

Proof state:
case h.e'_3
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
⊢ ↑(⨅ v, LinearMap.ker ((innerSL 𝕜) ↑v)) = ⋂ i, ↑(LinearMap.ker ((innerSL 𝕜) ↑i))

Tactic:
simp only [iInf_coe]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
⊢ IsClosed ↑Kᗮ

Tactic:
rw [orthogonal_eq_inter K]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
⊢ IsClosed ↑(⨅ v, LinearMap.ker ((innerSL 𝕜) ↑v))

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
⊢ IsClosed ↑(⨅ v, LinearMap.ker ((innerSL 𝕜) ↑v))

Tactic:
convert isClosed_iInter <| fun v : K => ContinuousLinearMap.isClosed_ker (innerSL 𝕜 (v : E))

Result:
case h.e'_3
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
⊢ ↑(⨅ v, LinearMap.ker ((innerSL 𝕜) ↑v)) = ⋂ i, ↑(LinearMap.ker ((innerSL 𝕜) ↑i))
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
lemma rpow_eq_zero (hy : y ≠ 0) : x ^ y = 0 ↔ x = 0

Proof state:
x : ℝ≥0
y : ℝ
hy : y ≠ 0
⊢ x ^ y = 0 ↔ x = 0

Tactic:
simp [hy]

Result:
no goals
-- Mathlib/Data/Finsupp/AList.lean
theorem _root_.Finsupp.toAList_lookupFinsupp (f : α →₀ M) : f.toAList.lookupFinsupp = f

Proof state:
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
⊢ f.toAList.lookupFinsupp = f

Tactic:
ext a

Result:
case h
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
⊢ f.toAList.lookupFinsupp a = f a

Proof state:
case pos
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : f a = 0
⊢ lookup a f.toAList = none

Tactic:
simp [lookup_eq_none, h]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : ¬f a = 0
this : lookup a f.toAList = some (f a)
⊢ f.toAList.lookupFinsupp a = f a

Tactic:
simp [h, this]

Result:
no goals

Proof state:
case neg
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : ¬f a = 0
⊢ f.toAList.lookupFinsupp a = f a

Tactic:
suffices f.toAList.lookup a = some (f a) by simp [h, this]

Result:
case neg
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : ¬f a = 0
⊢ lookup a f.toAList = some (f a)

Proof state:
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : f a = 0
this : lookup a f.toAList = none
⊢ f.toAList.lookupFinsupp a = f a

Tactic:
simp [h, this]

Result:
no goals

Proof state:
case neg
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : ¬f a = 0
⊢ ⟨a, f a⟩ ∈ f.toAList.entries

Tactic:
simpa using h

Result:
no goals

Proof state:
case neg
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : ¬f a = 0
⊢ lookup a f.toAList = some (f a)

Tactic:
apply mem_lookup_iff.2

Result:
case neg
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : ¬f a = 0
⊢ ⟨a, f a⟩ ∈ f.toAList.entries

Proof state:
case pos
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : f a = 0
⊢ f.toAList.lookupFinsupp a = f a

Tactic:
suffices f.toAList.lookup a = none by simp [h, this]

Result:
case pos
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : f a = 0
⊢ lookup a f.toAList = none

Proof state:
case h
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
⊢ f.toAList.lookupFinsupp a = f a

Tactic:
by_cases h : f a = 0

Result:
case pos
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : f a = 0
⊢ f.toAList.lookupFinsupp a = f a

case neg
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : ¬f a = 0
⊢ f.toAList.lookupFinsupp a = f a
-- Mathlib/Computability/Partrec.lean
theorem map_decode_iff {f : α → β → σ} :
    (Computable₂ fun a n => (decode (α := β) n).map (f a)) ↔ Computable₂ f

Proof state:
case h.e'_1.h.e'_7.h.h
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
x✝¹ : α
x✝ : ℕ
⊢ Option.map (f x✝¹) (decode x✝) = (decode x✝).bind (Option.some ∘ f x✝¹)

Tactic:
apply Option.map_eq_bind

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
⊢ (Computable₂ fun a n => Option.map (f a) (decode n)) ↔ Computable₂ f

Tactic:
convert (bind_decode_iff (f := fun a => Option.some ∘ f a)).trans option_some_iff

Result:
case h.e'_1.h.e'_7.h.h
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
x✝¹ : α
x✝ : ℕ
⊢ Option.map (f x✝¹) (decode x✝) = (decode x✝).bind (Option.some ∘ f x✝¹)
-- Mathlib/CategoryTheory/Bicategory/Adjunction/Mate.lean
theorem mateEquiv_hcomp (α : g ≫ l₂ ⟶ l₁ ≫ h) (β : h ≫ l₄ ⟶ l₃ ≫ k) :
    (mateEquiv (adj₁.comp adj₃) (adj₂.comp adj₄)) (leftAdjointSquare.hcomp α β) =
      rightAdjointSquare.hcomp (mateEquiv adj₁ adj₂ α) (mateEquiv adj₃ adj₄ β)

Proof state:
B : Type u
inst✝ : Bicategory B
a b c d e f : B
g : a ⟶ d
h : b ⟶ e
k : c ⟶ f
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : d ⟶ e
r₂ : e ⟶ d
l₃ : b ⟶ c
r₃ : c ⟶ b
l₄ : e ⟶ f
r₄ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
adj₄ : l₄ ⊣ r₄
α : g ≫ l₂ ⟶ l₁ ≫ h
β : h ≫ l₄ ⟶ l₃ ≫ k
⊢ 𝟙 ((r₃ ≫ r₁) ≫ g) ⊗≫
      (r₃ ≫ r₁) ◁ g ◁ (adj₂.unit ⊗≫ l₂ ◁ adj₄.unit ▷ r₂ ⊗≫ 𝟙 ((l₂ ≫ l₄) ≫ r₄ ≫ r₂)) ⊗≫
        (r₃ ≫ r₁) ◁ ((α_ g l₂ l₄).inv ≫ α ▷ l₄ ≫ (α_ l₁ h l₄).hom ≫ l₁ ◁ β ≫ (α_ l₁ l₃ k).inv) ▷ (r₄ ≫ r₂) ⊗≫
          (𝟙 ((r₃ ≫ r₁) ≫ l₁ ≫ l₃) ⊗≫ r₃ ◁ adj₁.counit ▷ l₃ ⊗≫ adj₃.counit) ▷ k ▷ (r₄ ≫ r₂) ⊗≫ 𝟙 (k ≫ r₄ ≫ r₂) =
    (α_ r₃ r₁ g).hom ≫
      r₃ ◁ (𝟙 (r₁ ≫ g) ⊗≫ r₁ ◁ g ◁ adj₂.unit ⊗≫ r₁ ◁ α ▷ r₂ ⊗≫ adj₁.counit ▷ h ▷ r₂ ⊗≫ 𝟙 (h ≫ r₂)) ≫
        (α_ r₃ h r₂).inv ≫
          (𝟙 (r₃ ≫ h) ⊗≫ r₃ ◁ h ◁ adj₄.unit ⊗≫ r₃ ◁ β ▷ r₄ ⊗≫ adj₃.counit ▷ k ▷ r₄ ⊗≫ 𝟙 (k ≫ r₄)) ▷ r₂ ≫
            (α_ k r₄ r₂).hom

Tactic:
calc
  _ = 𝟙 _ ⊗≫ r₃ ◁ r₁ ◁ g ◁ adj₂.unit ⊗≫
        r₃ ◁ r₁ ◁ ((g ≫ l₂) ◁ adj₄.unit ≫ α ▷ (l₄ ≫ r₄)) ▷ r₂ ⊗≫
          r₃ ◁ ((r₁ ≫ l₁) ◁ β ≫ adj₁.counit ▷ (l₃ ≫ k)) ▷ r₄ ▷ r₂ ⊗≫
            adj₃.counit ▷ k ▷ r₄ ▷ r₂ ⊗≫ 𝟙 _ := by
    bicategory
  _ = 𝟙 _ ⊗≫ r₃ ◁ r₁ ◁ g ◁ adj₂.unit ⊗≫ r₃ ◁ r₁ ◁ α ▷ r₂ ⊗≫
        r₃ ◁ ((r₁ ≫ l₁) ◁ h ◁ adj₄.unit ≫ adj₁.counit ▷ (h ≫ l₄ ≫ r₄)) ▷ r₂ ⊗≫
          r₃ ◁ β ▷ r₄ ▷ r₂ ⊗≫ adj₃.counit ▷ k ▷ r₄ ▷ r₂ ⊗≫ 𝟙 _ := by
    rw [whisker_exchange, whisker_exchange]
    bicategory
  _ = _ := by
    rw [whisker_exchange]
    bicategory

Result:
no goals
-- Mathlib/Analysis/Convex/Function.lean
theorem StrictConvexOn.translate_right (hf : StrictConvexOn 𝕜 s f) (c : E) :
    StrictConvexOn 𝕜 ((fun z => c + z) ⁻¹' s) (f ∘ fun z => c + z) :=
  ⟨hf.1.translate_preimage_right _, fun x hx y hy hxy a b ha hb hab =>
    calc
      f (c + (a • x + b • y)) = f (a • (c + x) + b • (c + y))

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCancelCommMonoid E
inst✝² : OrderedAddCommMonoid β
inst✝¹ : Module 𝕜 E
inst✝ : SMul 𝕜 β
s : Set E
f : E → β
hf : StrictConvexOn 𝕜 s f
c x : E
hx : x ∈ (fun z => c + z) ⁻¹' s
y : E
hy : y ∈ (fun z => c + z) ⁻¹' s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ f (c + (a • x + b • y)) = f (a • (c + x) + b • (c + y))

Tactic:
rw [smul_add, smul_add, add_add_add_comm, Convex.combo_self hab]

Result:
no goals
-- Mathlib/RingTheory/IsAdjoinRoot.lean
theorem coeff_apply_lt (h : IsAdjoinRootMonic S f) (z : S) (i : ℕ) (hi : i < natDegree f) :
    h.coeff z i = h.basis.repr z ⟨i, hi⟩

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
z : S
i : ℕ
hi : i < f.natDegree
⊢ { toFun := Polynomial.coeff, map_add' := ⋯ } (h.modByMonicHom z) i = (h.modByMonicHom z).coeff i

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
z : S
i : ℕ
hi : i < f.natDegree
⊢ h.coeff z i = (h.basis.repr z) ⟨i, hi⟩

Tactic:
simp only [coeff, LinearMap.comp_apply, Finsupp.lcoeFun_apply, Finsupp.lmapDomain_apply,
  LinearEquiv.coe_coe, liftPolyₗ_apply, LinearMap.coe_mk, h.basis_repr]

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
z : S
i : ℕ
hi : i < f.natDegree
⊢ { toFun := Polynomial.coeff, map_add' := ⋯ } (h.modByMonicHom z) i = (h.modByMonicHom z).coeff i
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem toIterator : ∀ {s}, ValidFor l m r s → s.toIterator.ValidFor l.reverse (m ++ r)
  | _, h => by
    simp only [Substring.toIterator]
    exact .of_eq _ (by simp [h.str, List.reverseAux_eq]) (by simp [h.startPos])

Proof state:
l m r : List Char
x✝ : Substring
h : ValidFor l m r x✝
⊢ Iterator.ValidFor l.reverse (m ++ r) { s := x✝.str, i := x✝.startPos }

Tactic:
exact .of_eq _ (by simp [h.str, List.reverseAux_eq]) (by simp [h.startPos])

Result:
no goals

Proof state:
l m r : List Char
x✝ : Substring
h : ValidFor l m r x✝
⊢ { s := x✝.str, i := x✝.startPos }.i.byteIdx = utf8Len l.reverse

Tactic:
simp [h.startPos]

Result:
no goals

Proof state:
l m r : List Char
x✝ : Substring
h : ValidFor l m r x✝
⊢ { s := x✝.str, i := x✝.startPos }.s.data = l.reverse.reverseAux (m ++ r)

Tactic:
simp [h.str, List.reverseAux_eq]

Result:
no goals

Proof state:
l m r : List Char
x✝ : Substring
h : ValidFor l m r x✝
⊢ Iterator.ValidFor l.reverse (m ++ r) x✝.toIterator

Tactic:
simp only [Substring.toIterator]

Result:
l m r : List Char
x✝ : Substring
h : ValidFor l m r x✝
⊢ Iterator.ValidFor l.reverse (m ++ r) { s := x✝.str, i := x✝.startPos }