harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/FreeCommRing.lean
theorem induction_on {C : FreeCommRing α → Prop} (z : FreeCommRing α) (hn1 : C (-1))
    (hb : ∀ b, C (of b)) (ha : ∀ x y, C x → C y → C (x + y)) (hm : ∀ x y, C x → C y → C (x * y)) :
    C z :=
  have hn : ∀ x, C x → C (-x) := fun x ih => neg_one_mul x ▸ hm _ _ hn1 ih
  have h1 : C 1 := neg_neg (1 : FreeCommRing α) ▸ hn _ hn1
  FreeAbelianGroup.induction_on z (neg_add_cancel (1 : FreeCommRing α) ▸ ha _ _ hn1 h1)
    (fun m => Multiset.induction_on m h1 fun a m ih => by
      convert hm (of a) _ (hb a) ih
      apply of_cons)
    (fun _ ih => hn _ ih) ha

Proof state:
α : Type u
C : FreeCommRing α → Prop
z : FreeCommRing α
hn1 : C (-1)
hb : ∀ (b : α), C (of b)
ha : ∀ (x y : FreeCommRing α), C x → C y → C (x + y)
hm : ∀ (x y : FreeCommRing α), C x → C y → C (x * y)
hn : ∀ (x : FreeCommRing α), C x → C (-x)
h1 : C 1
m✝ : Multiplicative (Multiset α)
a : α
m : Multiset α
ih : C (FreeAbelianGroup.of m)
⊢ C (FreeAbelianGroup.of (a ::ₘ m))

Tactic:
convert hm (of a) _ (hb a) ih

Result:
case h.e'_1
α : Type u
C : FreeCommRing α → Prop
z : FreeCommRing α
hn1 : C (-1)
hb : ∀ (b : α), C (of b)
ha : ∀ (x y : FreeCommRing α), C x → C y → C (x + y)
hm : ∀ (x y : FreeCommRing α), C x → C y → C (x * y)
hn : ∀ (x : FreeCommRing α), C x → C (-x)
h1 : C 1
m✝ : Multiplicative (Multiset α)
a : α
m : Multiset α
ih : C (FreeAbelianGroup.of m)
⊢ FreeAbelianGroup.of (a ::ₘ m) = of a * FreeAbelianGroup.of m

Proof state:
case h.e'_1
α : Type u
C : FreeCommRing α → Prop
z : FreeCommRing α
hn1 : C (-1)
hb : ∀ (b : α), C (of b)
ha : ∀ (x y : FreeCommRing α), C x → C y → C (x + y)
hm : ∀ (x y : FreeCommRing α), C x → C y → C (x * y)
hn : ∀ (x : FreeCommRing α), C x → C (-x)
h1 : C 1
m✝ : Multiplicative (Multiset α)
a : α
m : Multiset α
ih : C (FreeAbelianGroup.of m)
⊢ FreeAbelianGroup.of (a ::ₘ m) = of a * FreeAbelianGroup.of m

Tactic:
apply of_cons

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem isLittleO_congr (hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) : f₁ =o[l] g₁ ↔ f₂ =o[l] g₂

Proof state:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
⊢ (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₁ g₁) ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₂ g₂

Tactic:
exact forall₂_congr fun c _hc => isBigOWith_congr (Eq.refl c) hf hg

Result:
no goals

Proof state:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
⊢ f₁ =o[l] g₁ ↔ f₂ =o[l] g₂

Tactic:
simp only [IsLittleO_def]

Result:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
⊢ (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₁ g₁) ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₂ g₂
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
lemma toSubgraph_le_induce_support (p : G.Walk u v) :
    p.toSubgraph ≤ (⊤ : G.Subgraph).induce {v | v ∈ p.support}

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.toSubgraph ≤ ⊤.induce {v_1 | v_1 ∈ p.support}

Tactic:
convert Subgraph.le_induce_top_verts

Result:
case h.e'_4.h.e'_4
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ {v_1 | v_1 ∈ p.support} = p.toSubgraph.verts

Proof state:
case h.e'_4.h.e'_4
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ {v_1 | v_1 ∈ p.support} = p.toSubgraph.verts

Tactic:
exact p.verts_toSubgraph.symm

Result:
no goals
-- Mathlib/RingTheory/Ideal/Colon.lean
theorem mem_colon_singleton {N : Submodule R M} {x : M} {r : R} :
    r ∈ N.colon (Submodule.span R {x}) ↔ r • x ∈ N :=
  calc
    r ∈ N.colon (Submodule.span R {x}) ↔ ∀ a : R, r • a • x ∈ N

Proof state:
R : Type u_6
M : Type u_7
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
x : M
r : R
⊢ r ∈ N.colon (span R {x}) ↔ ∀ (a : R), r • a • x ∈ N

Tactic:
simp [Submodule.mem_colon, Submodule.mem_span_singleton]

Result:
no goals

Proof state:
R : Type u_6
M : Type u_7
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
x : M
r : R
⊢ (∀ (a : R), r • a • x ∈ N) ↔ r • x ∈ N

Tactic:
simp_rw [fun (a : R) ↦ smul_comm r a x]

Result:
R : Type u_6
M : Type u_7
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
x : M
r : R
⊢ (∀ (a : R), a • r • x ∈ N) ↔ r • x ∈ N

Proof state:
R : Type u_6
M : Type u_7
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
x : M
r : R
⊢ (∀ (a : R), a • r • x ∈ N) ↔ r • x ∈ N

Tactic:
exact SetLike.forall_smul_mem_iff

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
lemma succ_eq_of_lt_aleph0 {c : Cardinal} (h : c < ℵ₀) : Order.succ c = c + 1

Proof state:
c : Cardinal.{u_1}
h : c < ℵ₀
⊢ succ c = c + 1

Tactic:
obtain ⟨n, hn⟩ := Cardinal.lt_aleph0.mp h

Result:
case intro
c : Cardinal.{u_1}
h : c < ℵ₀
n : ℕ
hn : c = ↑n
⊢ succ c = c + 1

Proof state:
case intro
c : Cardinal.{u_1}
h : c < ℵ₀
n : ℕ
hn : c = ↑n
⊢ succ c = c + 1

Tactic:
rw [hn, succ_natCast]

Result:
no goals
-- Mathlib/LinearAlgebra/Ray.lean
theorem sameRay_smul_right_iff_of_ne {v : M} (hv : v ≠ 0) {r : R} (hr : r ≠ 0) :
    SameRay R v (r • v) ↔ 0 < r

Proof state:
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
v : M
hv : v ≠ 0
r : R
hr : r ≠ 0
⊢ SameRay R v (r • v) ↔ 0 < r

Tactic:
simp only [sameRay_smul_right_iff, hv, or_false, hr.symm.le_iff_lt]

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Basic.lean
theorem coeff_monomial [DecidableEq σ] (m n : σ →₀ ℕ) (a : R) :
    coeff R m (monomial R n a) = if m = n then a else 0

Proof state:
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : DecidableEq σ
m n : σ →₀ ℕ
a : R
⊢ (coeff R m) ((monomial R n) a) = if m = n then a else 0

Tactic:
erw [coeff, monomial_def, LinearMap.proj_apply (i := m)]

Result:
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : DecidableEq σ
m n : σ →₀ ℕ
a : R
⊢ (LinearMap.single R (fun x => R) n) a m = if m = n then a else 0

Proof state:
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : DecidableEq σ
m n : σ →₀ ℕ
a : R
⊢ (LinearMap.single R (fun x => R) n) a m = if m = n then a else 0

Tactic:
erw [LinearMap.single_apply, Pi.single_apply]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Pi.lean
@[simp]
lemma Fin.dist_insertNth_insertNth {n : ℕ} {α : Fin (n + 1) → Type*}
    [∀ i, PseudoMetricSpace (α i)] (i : Fin (n + 1)) (x y : α i) (f g : ∀ j, α (i.succAbove j)) :
    dist (i.insertNth x f) (i.insertNth y g) = max (dist x y) (dist f g)

Proof state:
n : ℕ
α : Fin (n + 1) → Type u_4
inst✝ : (i : Fin (n + 1)) → PseudoMetricSpace (α i)
i : Fin (n + 1)
x y : α i
f g : (j : Fin n) → α (i.succAbove j)
⊢ dist (i.insertNth x f) (i.insertNth y g) = dist x y ⊔ dist f g

Tactic:
simp only [dist_nndist, Fin.nndist_insertNth_insertNth, NNReal.coe_max]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Basic.lean
/-- If the `LSeries` of `f` is summable at `s`, then `f n` is bounded in absolute value
by a constant times `n^(re s)`. -/
lemma LSeriesSummable.le_const_mul_rpow {f : ℕ → ℂ} {s : ℂ} (h : LSeriesSummable f s) :
    ∃ C, ∀ n ≠ 0, ‖f n‖ ≤ C * n ^ s.re

Proof state:
f : ℕ → ℂ
s : ℂ
h : LSeriesSummable f s
⊢ ∃ C, ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ s.re

Tactic:
replace h := h.norm

Result:
f : ℕ → ℂ
s : ℂ
h : Summable fun x => ‖term f s x‖
⊢ ∃ C, ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ s.re

Proof state:
f : ℕ → ℂ
s : ℂ
h : Summable fun x => ‖term f s x‖
⊢ ∃ C, ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ s.re

Tactic:
by_contra! H

Result:
f : ℕ → ℂ
s : ℂ
h : Summable fun x => ‖term f s x‖
H : ∀ (C : ℝ), ∃ n, n ≠ 0 ∧ C * ↑n ^ s.re < ‖f n‖
⊢ False

Proof state:
f : ℕ → ℂ
s : ℂ
h : Summable fun x => ‖term f s x‖
H : ∀ (C : ℝ), ∃ n, n ≠ 0 ∧ C * ↑n ^ s.re < ‖f n‖
⊢ False

Tactic:
obtain ⟨n, hn₀, hn⟩ := H (tsum fun n ↦ ‖term f s n‖)

Result:
case intro.intro
f : ℕ → ℂ
s : ℂ
h : Summable fun x => ‖term f s x‖
H : ∀ (C : ℝ), ∃ n, n ≠ 0 ∧ C * ↑n ^ s.re < ‖f n‖
n : ℕ
hn₀ : n ≠ 0
hn : (∑' (n : ℕ), ‖term f s n‖) * ↑n ^ s.re < ‖f n‖
⊢ False

Proof state:
case intro.intro
f : ℕ → ℂ
s : ℂ
h : Summable fun x => ‖term f s x‖
H : ∀ (C : ℝ), ∃ n, n ≠ 0 ∧ C * ↑n ^ s.re < ‖f n‖
n : ℕ
hn₀ : n ≠ 0
hn : (∑' (n : ℕ), ‖term f s n‖) * ↑n ^ s.re < ‖f n‖
⊢ False

Tactic:
have := le_tsum h n fun _ _ ↦ norm_nonneg _

Result:
case intro.intro
f : ℕ → ℂ
s : ℂ
h : Summable fun x => ‖term f s x‖
H : ∀ (C : ℝ), ∃ n, n ≠ 0 ∧ C * ↑n ^ s.re < ‖f n‖
n : ℕ
hn₀ : n ≠ 0
hn : (∑' (n : ℕ), ‖term f s n‖) * ↑n ^ s.re < ‖f n‖
this : ‖term f s n‖ ≤ ∑' (i : ℕ), ‖term f s i‖
⊢ False

Proof state:
case intro.intro
f : ℕ → ℂ
s : ℂ
h : Summable fun x => ‖term f s x‖
H : ∀ (C : ℝ), ∃ n, n ≠ 0 ∧ C * ↑n ^ s.re < ‖f n‖
n : ℕ
hn₀ : n ≠ 0
hn : (∑' (n : ℕ), ‖term f s n‖) * ↑n ^ s.re < ‖f n‖
this : ‖term f s n‖ ≤ ∑' (i : ℕ), ‖term f s i‖
⊢ False

Tactic:
rw [norm_term_eq, if_neg hn₀,
  div_le_iff₀ <| Real.rpow_pos_of_pos (Nat.cast_pos.mpr <| Nat.pos_of_ne_zero hn₀) _] at this

Result:
case intro.intro
f : ℕ → ℂ
s : ℂ
h : Summable fun x => ‖term f s x‖
H : ∀ (C : ℝ), ∃ n, n ≠ 0 ∧ C * ↑n ^ s.re < ‖f n‖
n : ℕ
hn₀ : n ≠ 0
hn : (∑' (n : ℕ), ‖term f s n‖) * ↑n ^ s.re < ‖f n‖
this : ‖f n‖ ≤ (∑' (i : ℕ), ‖term f s i‖) * ↑n ^ s.re
⊢ False

Proof state:
case intro.intro
f : ℕ → ℂ
s : ℂ
h : Summable fun x => ‖term f s x‖
H : ∀ (C : ℝ), ∃ n, n ≠ 0 ∧ C * ↑n ^ s.re < ‖f n‖
n : ℕ
hn₀ : n ≠ 0
hn : (∑' (n : ℕ), ‖term f s n‖) * ↑n ^ s.re < ‖f n‖
this : ‖f n‖ ≤ (∑' (i : ℕ), ‖term f s i‖) * ↑n ^ s.re
⊢ False

Tactic:
exact (this.trans_lt hn).false.elim

Result:
no goals
-- Mathlib/Order/Category/HeytAlg.lean
lemma comp_apply {X Y Z : HeytAlg} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) :
    (f ≫ g) x = g (f x)

Proof state:
X Y Z : HeytAlg
f : X ⟶ Y
g : Y ⟶ Z
x : ↑X
⊢ (ConcreteCategory.hom (f ≫ g)) x = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x)

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/Spec.lean
theorem Spec.locallyRingedSpaceMap_id (R : CommRingCat.{u}) :
    Spec.locallyRingedSpaceMap (𝟙 R) = 𝟙 (Spec.locallyRingedSpaceObj R) :=
  LocallyRingedSpace.Hom.ext' <| by
    rw [Spec.locallyRingedSpaceMap_toShHom, Spec.sheafedSpaceMap_id]; rfl

Proof state:
R : CommRingCat
⊢ LocallyRingedSpace.Hom.toShHom (locallyRingedSpaceMap (𝟙 R)) =
    LocallyRingedSpace.Hom.toShHom (𝟙 (locallyRingedSpaceObj R))

Tactic:
rw [Spec.locallyRingedSpaceMap_toShHom, Spec.sheafedSpaceMap_id]

Result:
R : CommRingCat
⊢ 𝟙 (sheafedSpaceObj R) = LocallyRingedSpace.Hom.toShHom (𝟙 (locallyRingedSpaceObj R))

Proof state:
R : CommRingCat
⊢ 𝟙 (sheafedSpaceObj R) = LocallyRingedSpace.Hom.toShHom (𝟙 (locallyRingedSpaceObj R))

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/Interval/Finset/Nat.lean
theorem card_uIcc : #(uIcc a b) = (b - a : ℤ).natAbs + 1 :=
  (card_Icc _ _).trans <| by rw [← Int.natCast_inj, Int.ofNat_sub] <;> omega

Proof state:
a b : ℕ
⊢ a ⊔ b + 1 - a ⊓ b = (↑b - ↑a).natAbs + 1

Tactic:
rw [← Int.natCast_inj, Int.ofNat_sub] <;> omega

Result:
no goals
-- Mathlib/RingTheory/SimpleModule/Basic.lean
theorem eq_bot_or_exists_simple_le (N : Submodule R M) : N = ⊥ ∨ ∃ m ≤ N, IsSimpleModule R m

Proof state:
R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
N : Submodule R M
⊢ N = ⊥ ∨ ∃ m ≤ N, IsSimpleModule R ↥m

Tactic:
simpa only [isSimpleModule_iff_isAtom, and_comm] using eq_bot_or_exists_atom_le _

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem neg_lt_zero_iff {x : PGame} : -x < 0 ↔ 0 < x

Proof state:
x : PGame
⊢ -x < 0 ↔ 0 < x

Tactic:
rw [neg_lt_iff, neg_zero]

Result:
no goals
-- Mathlib/Algebra/Module/LinearMap/Polynomial.lean
@[simp]
lemma toMvPolynomial_constantCoeff (M : Matrix m n R) (i : m) :
    constantCoeff (M.toMvPolynomial i) = 0

Proof state:
m : Type u_1
n : Type u_2
R : Type u_4
inst✝¹ : Fintype n
inst✝ : CommSemiring R
M : Matrix m n R
i : m
⊢ constantCoeff (M.toMvPolynomial i) = 0

Tactic:
simp only [toMvPolynomial, ← C_mul_X_eq_monomial, map_sum, _root_.map_mul, constantCoeff_X,
  mul_zero, Finset.sum_const_zero]

Result:
no goals
-- Mathlib/RingTheory/IsAdjoinRoot.lean
theorem liftHom_map (h : IsAdjoinRoot S f) (z : R[X]) : h.liftHom x hx' (h.map z) = aeval x z

Proof state:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring S
f : R[X]
inst✝² : Algebra R S
T : Type u_1
inst✝¹ : CommRing T
x : T
inst✝ : Algebra R T
hx' : (aeval x) f = 0
h : IsAdjoinRoot S f
z : R[X]
⊢ (liftHom x hx' h) (h.map z) = (aeval x) z

Tactic:
rw [← lift_algebraMap_apply, lift_map, aeval_def]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem bsize : ∀ {s}, Valid s → s.bsize = utf8Len s.toString.1
  | _, h => let ⟨l, m, r, h⟩ := h.validFor; by simp [h.bsize, h.toString]

Proof state:
x✝ : Substring
h✝ : x✝.Valid
l m r : List Char
h : ValidFor l m r x✝
⊢ x✝.bsize = utf8Len x✝.toString.data

Tactic:
simp [h.bsize, h.toString]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Circulant.lean
theorem cycleGraph_two_eq_top : cycleGraph 2 = ⊤

Proof state:
⊢ ∀ (x x_1 : Fin 2), (cycleGraph 2).Adj x x_1 = ⊤.Adj x x_1

Tactic:
decide

Result:
no goals

Proof state:
⊢ cycleGraph 2 = ⊤

Tactic:
simp only [SimpleGraph.ext_iff, funext_iff]

Result:
⊢ ∀ (x x_1 : Fin 2), (cycleGraph 2).Adj x x_1 = ⊤.Adj x x_1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem findFinIdx?_congr {p : α → Bool} {l₁ : Array α} {l₂ : Array α} (w : l₁ = l₂) :
    findFinIdx? p l₁ = (findFinIdx? p l₂).map (fun i => i.cast (by simp [w]))

Proof state:
α : Type ?u.59116
p : α → Bool
l₁ l₂ : Array α
w : l₁ = l₂
i : Fin l₂.size
⊢ l₂.size = l₁.size

Tactic:
simp [w]

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
l₁ : Array α
⊢ findFinIdx? p l₁ = Option.map (fun i => Fin.cast ⋯ i) (findFinIdx? p l₁)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
l₁ l₂ : Array α
w : l₁ = l₂
⊢ findFinIdx? p l₁ = Option.map (fun i => Fin.cast ⋯ i) (findFinIdx? p l₂)

Tactic:
subst w

Result:
α : Type u_1
p : α → Bool
l₁ : Array α
⊢ findFinIdx? p l₁ = Option.map (fun i => Fin.cast ⋯ i) (findFinIdx? p l₁)
-- Mathlib/Topology/UniformSpace/Basic.lean
theorem uniformity_prod_eq_comap_prod [UniformSpace α] [UniformSpace β] :
    𝓤 (α × β) =
      comap (fun p : (α × β) × α × β => ((p.1.1, p.2.1), (p.1.2, p.2.2))) (𝓤 α ×ˢ 𝓤 β)

Proof state:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
⊢ 𝓤 (α × β) = Filter.comap (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 α ×ˢ 𝓤 β)

Tactic:
simp_rw [uniformity_prod, prod_eq_inf, Filter.comap_inf, Filter.comap_comap, Function.comp_def]

Result:
no goals
-- Mathlib/Data/Fintype/EquivFin.lean
theorem nonempty (α : Type*) [Infinite α] : Nonempty α

Proof state:
α : Type u_4
inst✝ : Infinite α
⊢ Nonempty α

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Data/Matrix/Kronecker.lean
theorem kroneckerMap_diagonal_left [Zero α] [Zero γ] [DecidableEq l] (f : α → β → γ)
    (hf : ∀ b, f 0 b = 0) (a : l → α) (B : Matrix m n β) :
    kroneckerMap f (diagonal a) B =
      Matrix.reindex (Equiv.prodComm _ _) (Equiv.prodComm _ _)
        (blockDiagonal fun i => B.map fun b => f (a i) b)

Proof state:
case a.mk.mk
α : Type u_2
β : Type u_4
γ : Type u_6
l : Type u_8
m : Type u_9
n : Type u_10
inst✝² : Zero α
inst✝¹ : Zero γ
inst✝ : DecidableEq l
f : α → β → γ
hf : ∀ (b : β), f 0 b = 0
a : l → α
B : Matrix m n β
i₁ : l
i₂ : m
j₁ : l
j₂ : n
⊢ kroneckerMap f (diagonal a) B (i₁, i₂) (j₁, j₂) =
    (reindex (Equiv.prodComm m l) (Equiv.prodComm n l)) (blockDiagonal fun i => B.map fun b => f (a i) b) (i₁, i₂)
      (j₁, j₂)

Tactic:
simp [diagonal, blockDiagonal, apply_ite f, ite_apply, hf]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_4
γ : Type u_6
l : Type u_8
m : Type u_9
n : Type u_10
inst✝² : Zero α
inst✝¹ : Zero γ
inst✝ : DecidableEq l
f : α → β → γ
hf : ∀ (b : β), f 0 b = 0
a : l → α
B : Matrix m n β
⊢ kroneckerMap f (diagonal a) B =
    (reindex (Equiv.prodComm m l) (Equiv.prodComm n l)) (blockDiagonal fun i => B.map fun b => f (a i) b)

Tactic:
ext ⟨i₁, i₂⟩ ⟨j₁, j₂⟩

Result:
case a.mk.mk
α : Type u_2
β : Type u_4
γ : Type u_6
l : Type u_8
m : Type u_9
n : Type u_10
inst✝² : Zero α
inst✝¹ : Zero γ
inst✝ : DecidableEq l
f : α → β → γ
hf : ∀ (b : β), f 0 b = 0
a : l → α
B : Matrix m n β
i₁ : l
i₂ : m
j₁ : l
j₂ : n
⊢ kroneckerMap f (diagonal a) B (i₁, i₂) (j₁, j₂) =
    (reindex (Equiv.prodComm m l) (Equiv.prodComm n l)) (blockDiagonal fun i => B.map fun b => f (a i) b) (i₁, i₂)
      (j₁, j₂)
-- Mathlib/FieldTheory/PerfectClosure.lean
theorem add_aux_right (x y1 y2 : ℕ × K) (H : R K p y1 y2) :
    mk K p (x.1 + y1.1, (frobenius K p)^[y1.1] x.2 + (frobenius K p)^[x.1] y1.2) =
      mk K p (x.1 + y2.1, (frobenius K p)^[y2.1] x.2 + (frobenius K p)^[x.1] y2.2) :=
  match y1, y2, H with
  | _, _, R.intro n y =>
    Quot.sound <| by
      rw [← iterate_succ_apply, iterate_succ_apply', iterate_succ_apply', ← frobenius_add]
      apply R.intro

Proof state:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y1 y2 : ℕ × K
H : R K p y1 y2
n : ℕ
y : K
⊢ R K p (x.1 + (n, y).1, (⇑(frobenius K p))^[(n, y).1] x.2 + (⇑(frobenius K p))^[x.1] (n, y).2)
    (x.1 + (n + 1, (frobenius K p) y).1, (frobenius K p) ((⇑(frobenius K p))^[n] x.2 + (⇑(frobenius K p))^[x.1] y))

Tactic:
apply R.intro

Result:
no goals

Proof state:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y1 y2 : ℕ × K
H : R K p y1 y2
n : ℕ
y : K
⊢ R K p (x.1 + (n, y).1, (⇑(frobenius K p))^[(n, y).1] x.2 + (⇑(frobenius K p))^[x.1] (n, y).2)
    (x.1 + (n + 1, (frobenius K p) y).1,
      (⇑(frobenius K p))^[(n + 1, (frobenius K p) y).1] x.2 + (⇑(frobenius K p))^[x.1] (n + 1, (frobenius K p) y).2)

Tactic:
rw [← iterate_succ_apply, iterate_succ_apply', iterate_succ_apply', ← frobenius_add]

Result:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y1 y2 : ℕ × K
H : R K p y1 y2
n : ℕ
y : K
⊢ R K p (x.1 + (n, y).1, (⇑(frobenius K p))^[(n, y).1] x.2 + (⇑(frobenius K p))^[x.1] (n, y).2)
    (x.1 + (n + 1, (frobenius K p) y).1, (frobenius K p) ((⇑(frobenius K p))^[n] x.2 + (⇑(frobenius K p))^[x.1] y))
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
lemma integrable_const_iff {c : β} : Integrable (fun _ : α => c) μ ↔ c = 0 ∨ IsFiniteMeasure μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
c : β
⊢ Integrable (fun x => c) μ ↔ c = 0 ∨ IsFiniteMeasure μ

Tactic:
have : AEStronglyMeasurable (fun _ : α => c) μ := aestronglyMeasurable_const

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
c : β
this : AEStronglyMeasurable (fun x => c) μ
⊢ Integrable (fun x => c) μ ↔ c = 0 ∨ IsFiniteMeasure μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
c : β
this : AEStronglyMeasurable (fun x => c) μ
⊢ Integrable (fun x => c) μ ↔ c = 0 ∨ IsFiniteMeasure μ

Tactic:
rw [Integrable, and_iff_right this, hasFiniteIntegral_const_iff]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem mul_inv_le_iff_le_mul' : a * b⁻¹ ≤ c ↔ a ≤ b * c

Proof state:
α : Type u
inst✝² : CommGroup α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a b c : α
⊢ a * b⁻¹ ≤ c ↔ a ≤ b * c

Tactic:
rw [← inv_mul_le_iff_le_mul, mul_comm]

Result:
no goals
-- Mathlib/RingTheory/Kaehler/CotangentComplex.lean
lemma cotangentSpaceBasis_repr_one_tmul (x i) :
    P.cotangentSpaceBasis.repr (1 ⊗ₜ .D _ _ x) i = aeval P.val (pderiv i x)

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Generators R S
x : P.toExtension.Ring
i : P.vars
⊢ (P.cotangentSpaceBasis.repr (1 ⊗ₜ[P.toExtension.Ring] (D R P.toExtension.Ring) x)) i = (aeval P.val) ((pderiv i) x)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/Commute/Units.lean
@[to_additive]
lemma Commute.div_eq_div_iff_of_isUnit (hbd : Commute b d) (hb : IsUnit b) (hd : IsUnit d) :
    a / b = c / d ↔ a * d = c * b

Proof state:
M : Type u_1
inst✝ : DivisionMonoid M
a b c d : M
hbd : Commute b d
hb : IsUnit b
hd : IsUnit d
⊢ a / b = c / d ↔ a * d = c * b

Tactic:
rw [← (hb.mul hd).mul_left_inj, ← mul_assoc, hb.div_mul_cancel, ← mul_assoc, hbd.right_comm,
  hd.div_mul_cancel]

Result:
no goals
-- Mathlib/Order/OrdContinuous.lean
theorem mono (hf : LeftOrdContinuous f) : Monotone f := fun a₁ a₂ h =>
  have : IsGreatest {a₁, a₂} a₂ := ⟨Or.inr rfl, by simp [*]⟩
  (hf.map_isGreatest this).2 <| mem_image_of_mem _ (Or.inl rfl)

Proof state:
α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : LeftOrdContinuous f
a₁ a₂ : α
h : a₁ ≤ a₂
⊢ a₂ ∈ upperBounds {a₁, a₂}

Tactic:
simp [*]

Result:
no goals
-- Mathlib/Algebra/Algebra/Unitization.lean
theorem inr_mul_inl [Semiring R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] (r : R)
    (a : A) : a * (inl r : Unitization R A) = ↑(r • a) :=
  ext (zero_mul r) <|
    show (0 : R) • (0 : A) + r • a + a * 0 = r • a by
      rw [smul_zero, zero_add, mul_zero, add_zero]

Proof state:
R : Type u_1
A : Type u_2
inst✝² : Semiring R
inst✝¹ : NonUnitalNonAssocSemiring A
inst✝ : DistribMulAction R A
r : R
a : A
⊢ 0 • 0 + r • a + a * 0 = r • a

Tactic:
rw [smul_zero, zero_add, mul_zero, add_zero]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Basic.lean
lemma pow_eq_zero_of_le : ∀ {m n}, m ≤ n → a ^ m = 0 → a ^ n = 0
  | _, _, Nat.le.refl, ha => ha
  | _, _, Nat.le.step hmn, ha => by rw [pow_succ, pow_eq_zero_of_le hmn ha, zero_mul]

Proof state:
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a : M₀
n✝ m✝ : ℕ
hmn : n✝.le m✝
ha : a ^ n✝ = 0
⊢ a ^ m✝.succ = 0

Tactic:
rw [pow_succ, pow_eq_zero_of_le hmn ha, zero_mul]

Result:
no goals
-- Mathlib/Algebra/Ring/Parity.lean
lemma Even.add_odd : Even a → Odd b → Odd (a + b)

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

Tactic:
exact ⟨a + b, by rw [mul_add, ← two_mul, add_assoc]⟩

Result:
no goals

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

Tactic:
rw [mul_add, ← two_mul, add_assoc]

Result:
no goals

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

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

Result:
case intro.intro
α : Type u_2
inst✝ : Semiring α
a b : α
⊢ Odd (a + a + (2 * b + 1))
-- Mathlib/Algebra/Lie/CartanMatrix.lean
theorem adE_of_eq_eq_zero (i : B) (h : A i i = 2) : adE R A ⟨i, i⟩ = 0

Proof state:
R : Type u
B : Type v
inst✝ : CommRing R
A : Matrix B B ℤ
i : B
h : A i i = 2
h' : (-2).toNat = 0
⊢ adE R A (i, i) = 0

Tactic:
simp [adE, h, h']

Result:
no goals

Proof state:
R : Type u
B : Type v
inst✝ : CommRing R
A : Matrix B B ℤ
i : B
h : A i i = 2
⊢ adE R A (i, i) = 0

Tactic:
have h' : (-2 : ℤ).toNat = 0 := rfl

Result:
R : Type u
B : Type v
inst✝ : CommRing R
A : Matrix B B ℤ
i : B
h : A i i = 2
h' : (-2).toNat = 0
⊢ adE R A (i, i) = 0
-- Mathlib/Algebra/CubicDiscriminant.lean
theorem degree_of_d_ne_zero (ha : P.a = 0) (hb : P.b = 0) (hc : P.c = 0) (hd : P.d ≠ 0) :
    P.toPoly.degree = 0

Proof state:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c = 0
hd : P.d ≠ 0
⊢ P.toPoly.degree = 0

Tactic:
rw [of_c_eq_zero ha hb hc, degree_C hd]

Result:
no goals