harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/HalesJewett.lean
theorem diagonal_apply {α ι} [Nonempty ι] (x : α) : diagonal α ι x = fun _ => x

Proof state:
case h
α : Type u_5
ι : Type u_6
inst✝ : Nonempty ι
x : α
x✝ : ι
⊢ ↑(diagonal α ι) x x✝ = x

Tactic:
simp [diagonal]

Result:
no goals

Proof state:
α : Type u_5
ι : Type u_6
inst✝ : Nonempty ι
x : α
⊢ ↑(diagonal α ι) x = fun x_1 => x

Tactic:
ext

Result:
case h
α : Type u_5
ι : Type u_6
inst✝ : Nonempty ι
x : α
x✝ : ι
⊢ ↑(diagonal α ι) x x✝ = x
-- Mathlib/Order/WithBot.lean
lemma unbotD_lt_iff (hx : x = ⊥ → a < b) : x.unbotD a < b ↔ x < b

Proof state:
α : Type u_1
a b : α
inst✝ : LT α
x : WithBot α
hx : x = ⊥ → a < b
⊢ unbotD a x < b ↔ x < ↑b

Tactic:
cases x <;> simp [hx]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Pairwise.lean
theorem pairwise_append_comm {R : α → α → Prop} (s : ∀ {x y}, R x y → R y x) {l₁ l₂ : List α} :
    Pairwise R (l₁ ++ l₂) ↔ Pairwise R (l₂ ++ l₁)

Proof state:
α : Type u_1
R : α → α → Prop
s : ∀ {x y : α}, R x y → R y x
l₁ l₂ : List α
this :
  ∀ (l₁ l₂ : List α), (∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y) → ∀ (x : α), x ∈ l₂ → ∀ (y : α), y ∈ l₁ → R x y
⊢ Pairwise R (l₁ ++ l₂) ↔ Pairwise R (l₂ ++ l₁)

Tactic:
simp only [pairwise_append, and_left_comm]

Result:
α : Type u_1
R : α → α → Prop
s : ∀ {x y : α}, R x y → R y x
l₁ l₂ : List α
this :
  ∀ (l₁ l₂ : List α), (∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y) → ∀ (x : α), x ∈ l₂ → ∀ (y : α), y ∈ l₁ → R x y
⊢ (Pairwise R l₁ ∧ Pairwise R l₂ ∧ ∀ (a : α), a ∈ l₁ → ∀ (b : α), b ∈ l₂ → R a b) ↔
    Pairwise R l₁ ∧ Pairwise R l₂ ∧ ∀ (a : α), a ∈ l₂ → ∀ (b : α), b ∈ l₁ → R a b

Proof state:
α : Type u_1
R : α → α → Prop
s : ∀ {x y : α}, R x y → R y x
l₁ l₂ : List α
this :
  ∀ (l₁ l₂ : List α), (∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y) → ∀ (x : α), x ∈ l₂ → ∀ (y : α), y ∈ l₁ → R x y
⊢ (Pairwise R l₁ ∧ Pairwise R l₂ ∧ ∀ (a : α), a ∈ l₁ → ∀ (b : α), b ∈ l₂ → R a b) ↔
    Pairwise R l₁ ∧ Pairwise R l₂ ∧ ∀ (a : α), a ∈ l₂ → ∀ (b : α), b ∈ l₁ → R a b

Tactic:
rw [Iff.intro (this l₁ l₂) (this l₂ l₁)]

Result:
no goals

Proof state:
α : Type u_1
R : α → α → Prop
s : ∀ {x y : α}, R x y → R y x
l₁ l₂ : List α
⊢ Pairwise R (l₁ ++ l₂) ↔ Pairwise R (l₂ ++ l₁)

Tactic:
have (l₁ l₂ : List α) (H : ∀ x : α, x ∈ l₁ → ∀ y : α, y ∈ l₂ → R x y)
  (x : α) (xm : x ∈ l₂) (y : α) (ym : y ∈ l₁) : R x y := s (H y ym x xm)

Result:
α : Type u_1
R : α → α → Prop
s : ∀ {x y : α}, R x y → R y x
l₁ l₂ : List α
this :
  ∀ (l₁ l₂ : List α), (∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y) → ∀ (x : α), x ∈ l₂ → ∀ (y : α), y ∈ l₁ → R x y
⊢ Pairwise R (l₁ ++ l₂) ↔ Pairwise R (l₂ ++ l₁)
-- Mathlib/Order/Category/FinPartOrd.lean
lemma id_apply (X : FinPartOrd) (x : X) :
    (𝟙 X : X ⟶ X) x = x

Proof state:
X : FinPartOrd
x : ↑X.toPartOrd
⊢ (ConcreteCategory.hom (𝟙 X)) x = x

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Kleene.lean
theorem add_idem (a : α) : a + a = a

Proof state:
α : Type u_1
inst✝ : IdemSemiring α
a : α
⊢ a + a = a

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/EvenOddRec.lean
theorem evenOddRec_odd {P : ℕ → Sort*} (h0 : P 0) (h_even : ∀ i, P i → P (2 * i))
    (h_odd : ∀ i, P i → P (2 * i + 1)) (H : h_even 0 h0 = h0) (n : ℕ) :
    (2 * n + 1).evenOddRec h0 h_even h_odd = h_odd n (evenOddRec h0 h_even h_odd n)

Proof state:
P : ℕ → Sort u_1
h0 : P 0
h_even : (i : ℕ) → P i → P (2 * i)
h_odd : (i : ℕ) → P i → P (2 * i + 1)
H : h_even 0 h0 = h0
n : ℕ
⊢ evenOddRec h0 h_even h_odd (2 * n + 1) = h_odd n (evenOddRec h0 h_even h_odd n)

Tactic:
apply binaryRec_eq true n

Result:
P : ℕ → Sort u_1
h0 : P 0
h_even : (i : ℕ) → P i → P (2 * i)
h_odd : (i : ℕ) → P i → P (2 * i + 1)
H : h_even 0 h0 = h0
n : ℕ
⊢ (match false, 0, h0 with
      | false, i, hi => h_even i hi
      | true, i, hi => h_odd i hi) =
      h0 ∨
    (n = 0 → true = true)

Proof state:
P : ℕ → Sort u_1
h0 : P 0
h_even : (i : ℕ) → P i → P (2 * i)
h_odd : (i : ℕ) → P i → P (2 * i + 1)
H : h_even 0 h0 = h0
n : ℕ
⊢ (match false, 0, h0 with
      | false, i, hi => h_even i hi
      | true, i, hi => h_odd i hi) =
      h0 ∨
    (n = 0 → true = true)

Tactic:
simp [H]

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem bihimp_of_ge {a b : α} (h : b ≤ a) : a ⇔ b = a ⇨ b

Proof state:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
h : b ≤ a
⊢ a ⇔ b = a ⇨ b

Tactic:
rw [bihimp, himp_eq_top_iff.2 h, top_inf_eq]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Pointwise.lean
theorem singleton_mul_ball : {x} * ball y δ = ball (x * y) δ

Proof state:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x y : E
⊢ {x} * ball y δ = ball (x * y) δ

Tactic:
simp only [preimage_mul_ball, image_mul_left, singleton_mul, div_inv_eq_mul, mul_comm y x]

Result:
no goals
-- Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean
theorem sum_add_index' {S : Type*} [AddCommMonoid S] {f g : SkewMonoidAlgebra k G} {h : G → k → S}
    (hf : ∀ i, h i 0 = 0) (h_add : ∀ a b₁ b₂, h a (b₁ + b₂) = h a b₁ + h a b₂) :
    (f + g).sum h = f.sum h + g.sum h

Proof state:
k : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid k
S : Type u_3
inst✝ : AddCommMonoid S
f g : SkewMonoidAlgebra k G
h : G → k → S
hf : ∀ (i : G), h i 0 = 0
h_add : ∀ (a : G) (b₁ b₂ : k), h a (b₁ + b₂) = h a b₁ + h a b₂
⊢ f + g = { toFinsupp := f.toFinsupp + g.toFinsupp }

Tactic:
rw [ofFinsupp_add, eta]

Result:
no goals

Proof state:
k : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid k
S : Type u_3
inst✝ : AddCommMonoid S
f g : SkewMonoidAlgebra k G
h : G → k → S
hf : ∀ (i : G), h i 0 = 0
h_add : ∀ (a : G) (b₁ b₂ : k), h a (b₁ + b₂) = h a b₁ + h a b₂
⊢ (f + g).sum h = f.sum h + g.sum h

Tactic:
rw [show f + g = ⟨f.toFinsupp + g.toFinsupp⟩ by rw [ofFinsupp_add, eta]]

Result:
k : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid k
S : Type u_3
inst✝ : AddCommMonoid S
f g : SkewMonoidAlgebra k G
h : G → k → S
hf : ∀ (i : G), h i 0 = 0
h_add : ∀ (a : G) (b₁ b₂ : k), h a (b₁ + b₂) = h a b₁ + h a b₂
⊢ { toFinsupp := f.toFinsupp + g.toFinsupp }.sum h = f.sum h + g.sum h

Proof state:
k : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid k
S : Type u_3
inst✝ : AddCommMonoid S
f g : SkewMonoidAlgebra k G
h : G → k → S
hf : ∀ (i : G), h i 0 = 0
h_add : ∀ (a : G) (b₁ b₂ : k), h a (b₁ + b₂) = h a b₁ + h a b₂
⊢ { toFinsupp := f.toFinsupp + g.toFinsupp }.sum h = f.sum h + g.sum h

Tactic:
exact Finsupp.sum_add_index' hf h_add

Result:
no goals
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem map_one_add (x : ℝ) : f (1 + x) = 1 + f x

Proof state:
f : CircleDeg1Lift
x : ℝ
⊢ f (1 + x) = 1 + f x

Tactic:
rw [add_comm, map_add_one, add_comm 1]

Result:
no goals
-- Mathlib/Data/Finsupp/SMul.lean
theorem support_smul_eq [Semiring R] [AddCommMonoid M] [Module R M] [NoZeroSMulDivisors R M] {b : R}
    (hb : b ≠ 0) {g : α →₀ M} : (b • g).support = g.support :=
  Finset.ext fun a => by simp [Finsupp.smul_apply, hb]

Proof state:
α : Type u_1
M : Type u_3
R : Type u_6
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
b : R
hb : b ≠ 0
g : α →₀ M
a : α
⊢ a ∈ (b • g).support ↔ a ∈ g.support

Tactic:
simp [Finsupp.smul_apply, hb]

Result:
no goals
-- Mathlib/Data/Set/Basic.lean
theorem inclusion_right (h : s ⊆ t) (x : t) (m : (x : α) ∈ s) : inclusion h ⟨x, m⟩ = x

Proof state:
case mk
α : Type u_1
s t : Set α
h : s ⊆ t
val✝ : α
property✝ : val✝ ∈ t
m : ↑⟨val✝, property✝⟩ ∈ s
⊢ inclusion h ⟨↑⟨val✝, property✝⟩, m⟩ = ⟨val✝, property✝⟩

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
s t : Set α
h : s ⊆ t
x : ↑t
m : ↑x ∈ s
⊢ inclusion h ⟨↑x, m⟩ = x

Tactic:
cases x

Result:
case mk
α : Type u_1
s t : Set α
h : s ⊆ t
val✝ : α
property✝ : val✝ ∈ t
m : ↑⟨val✝, property✝⟩ ∈ s
⊢ inclusion h ⟨↑⟨val✝, property✝⟩, m⟩ = ⟨val✝, property✝⟩
-- Mathlib/Data/Set/Basic.lean
theorem not_nonempty_iff_eq_empty' : ¬Nonempty s ↔ s = ∅

Proof state:
α : Type u
s : Set α
⊢ ¬Nonempty ↑s ↔ s = ∅

Tactic:
rw [nonempty_subtype, not_exists, eq_empty_iff_forall_not_mem]

Result:
no goals
-- Mathlib/Algebra/Module/ZLattice/Covolume.lean
theorem covolume_eq_measure_fundamentalDomain {F : Set E} (h : IsAddFundamentalDomain L F μ) :
    covolume L μ = (μ F).toReal

Proof state:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
L : Submodule ℤ E
inst✝² : DiscreteTopology ↥L
inst✝¹ : IsZLattice ℝ L
μ : autoParam (Measure E) _auto✝
inst✝ : Measure.IsAddHaarMeasure μ
F : Set E
h : IsAddFundamentalDomain (↥L) F μ
⊢ covolume L μ = (μ F).toReal

Tactic:
have : MeasurableVAdd L E := (inferInstance : MeasurableVAdd L.toAddSubgroup E)

Result:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
L : Submodule ℤ E
inst✝² : DiscreteTopology ↥L
inst✝¹ : IsZLattice ℝ L
μ : autoParam (Measure E) _auto✝
inst✝ : Measure.IsAddHaarMeasure μ
F : Set E
h : IsAddFundamentalDomain (↥L) F μ
this : MeasurableVAdd (↥L) E
⊢ covolume L μ = (μ F).toReal

Proof state:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
L : Submodule ℤ E
inst✝² : DiscreteTopology ↥L
inst✝¹ : IsZLattice ℝ L
μ : autoParam (Measure E) _auto✝
inst✝ : Measure.IsAddHaarMeasure μ
F : Set E
h : IsAddFundamentalDomain (↥L) F μ
this✝ : MeasurableVAdd (↥L) E
this : VAddInvariantMeasure (↥L) E μ
⊢ covolume L μ = (μ F).toReal

Tactic:
exact congr_arg ENNReal.toReal (h.covolume_eq_volume μ)

Result:
no goals

Proof state:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
L : Submodule ℤ E
inst✝² : DiscreteTopology ↥L
inst✝¹ : IsZLattice ℝ L
μ : autoParam (Measure E) _auto✝
inst✝ : Measure.IsAddHaarMeasure μ
F : Set E
h : IsAddFundamentalDomain (↥L) F μ
this : MeasurableVAdd (↥L) E
⊢ covolume L μ = (μ F).toReal

Tactic:
have : VAddInvariantMeasure L E μ := (inferInstance : VAddInvariantMeasure L.toAddSubgroup E μ)

Result:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
L : Submodule ℤ E
inst✝² : DiscreteTopology ↥L
inst✝¹ : IsZLattice ℝ L
μ : autoParam (Measure E) _auto✝
inst✝ : Measure.IsAddHaarMeasure μ
F : Set E
h : IsAddFundamentalDomain (↥L) F μ
this✝ : MeasurableVAdd (↥L) E
this : VAddInvariantMeasure (↥L) E μ
⊢ covolume L μ = (μ F).toReal
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem cos_sub_pi_div_two (x : ℂ) : cos (x - π / 2) = sin x

Proof state:
x : ℂ
⊢ cos (x - ↑π / 2) = sin x

Tactic:
simp [sub_eq_add_neg, cos_add]

Result:
no goals
-- Mathlib/Order/Interval/Set/OrdConnected.lean
lemma not_ordConnected_inter_Icc_iff (hx : x ∈ s) (hy : y ∈ s) :
    ¬ OrdConnected (s ∩ Icc x y) ↔ ∃ z ∉ s, z ∈ Ioo x y

Proof state:
α : Type u_1
inst✝ : PartialOrder α
s : Set α
x y : α
hx : x ∈ s
hy : y ∈ s
⊢ ¬(s ∩ Icc x y).OrdConnected ↔ ∃ z ∉ s, z ∈ Ioo x y

Tactic:
simp_rw [ordConnected_inter_Icc_iff hx hy, subset_def, not_forall, exists_prop, and_comm]

Result:
no goals
-- Mathlib/Data/Vector/Basic.lean
theorem nodup_iff_injective_get {v : Vector α n} : v.toList.Nodup ↔ Function.Injective v.get

Proof state:
α : Type u_1
n : ℕ
v : Vector α n
⊢ v.toList.Nodup ↔ Function.Injective v.get

Tactic:
obtain ⟨l, hl⟩ := v

Result:
case mk
α : Type u_1
n : ℕ
l : List α
hl : l.length = n
⊢ (toList ⟨l, hl⟩).Nodup ↔ Function.Injective (get ⟨l, hl⟩)

Proof state:
case mk
α : Type u_1
l : List α
⊢ (toList ⟨l, ⋯⟩).Nodup ↔ Function.Injective (get ⟨l, ⋯⟩)

Tactic:
exact List.nodup_iff_injective_get

Result:
no goals

Proof state:
case mk
α : Type u_1
n : ℕ
l : List α
hl : l.length = n
⊢ (toList ⟨l, hl⟩).Nodup ↔ Function.Injective (get ⟨l, hl⟩)

Tactic:
subst hl

Result:
case mk
α : Type u_1
l : List α
⊢ (toList ⟨l, ⋯⟩).Nodup ↔ Function.Injective (get ⟨l, ⋯⟩)
-- Mathlib/Algebra/Lie/Abelian.lean
theorem LieSubmodule.lie_abelian_iff_lie_self_eq_bot : IsLieAbelian I ↔ ⁅I, I⁆ = ⊥

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
h : IsLieAbelian ↥I
z : L
x y : ↥I
hz : ⁅↑x, ↑y⁆ = z
⊢ ⁅x, y⁆ = 0

Tactic:
apply h.trivial

Result:
no goals

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ IsLieAbelian ↥I ↔ ∀ (y : L) (x x_1 : ↥I), ⁅↑x, ↑x_1⁆ = y → y = 0

Tactic:
refine
  ⟨fun h z x y hz =>
    hz.symm.trans
      (((I : LieSubalgebra R L).coe_bracket x y).symm.trans
        ((coe_zero_iff_zero _ _).mpr (by apply h.trivial))),
    fun h => ⟨fun x y => ((I : LieSubalgebra R L).coe_zero_iff_zero _).mp (h _ x y rfl)⟩⟩

Result:
no goals

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ IsLieAbelian ↥I ↔ ⁅I, I⁆ = ⊥

Tactic:
simp only [_root_.eq_bot_iff, lieIdeal_oper_eq_span, LieSubmodule.lieSpan_le,
  LieSubmodule.bot_coe, Set.subset_singleton_iff, Set.mem_setOf_eq, exists_imp]

Result:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ IsLieAbelian ↥I ↔ ∀ (y : L) (x x_1 : ↥I), ⁅↑x, ↑x_1⁆ = y → y = 0
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma abs_cpow_inv_two_im (x : ℂ) : |(x ^ (2⁻¹ : ℂ)).im| = sqrt ((‖x‖ - x.re) / 2)

Proof state:
x : ℂ
⊢ |(x ^ 2⁻¹).im| = √((‖x‖ - x.re) / 2)

Tactic:
rw [← ofReal_ofNat, ← ofReal_inv, cpow_ofReal_im, ← div_eq_mul_inv, ← one_div,
  ← Real.sqrt_eq_rpow, abs_mul, abs_of_nonneg (sqrt_nonneg _), abs_sin_half,
  ← sqrt_mul (norm_nonneg _), ← mul_div_assoc, mul_sub, mul_one, norm_mul_cos_arg]

Result:
no goals
-- Mathlib/Data/DFinsupp/BigOperators.lean
theorem liftAddHom_comp_single [∀ i, AddZeroClass (β i)] [AddCommMonoid γ] (f : ∀ i, β i →+ γ)
    (i : ι) : (liftAddHom (β := β) f).comp (singleAddHom β i) = f i

Proof state:
ι : Type u
γ : Type w
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
f : (i : ι) → β i →+ γ
i : ι
⊢ (liftAddHom f).comp (singleAddHom β i) = f i

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/DiscreteValuationRing/Basic.lean
theorem irreducible_iff_uniformizer (ϖ : R) : Irreducible ϖ ↔ maximalIdeal R = Ideal.span {ϖ} :=
  ⟨fun hϖ => (eq_maximalIdeal (isMaximal_of_irreducible hϖ)).symm,
    fun h => irreducible_of_span_eq_maximalIdeal ϖ
      (fun e => not_a_field R <| by rwa [h, span_singleton_eq_bot]) h⟩

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
h : maximalIdeal R = span {ϖ}
e : ϖ = 0
⊢ maximalIdeal R = ⊥

Tactic:
rwa [h, span_singleton_eq_bot]

Result:
no goals
-- Mathlib/Algebra/Lie/Nilpotent.lean
@[simp]
lemma lcs_sup {N₁ N₂ : LieSubmodule R L M} {k : ℕ} :
    (N₁ ⊔ N₂).lcs k = N₁.lcs k ⊔ N₂.lcs k

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N₁ N₂ : LieSubmodule R L M
k : ℕ
⊢ lcs k (N₁ ⊔ N₂) = lcs k N₁ ⊔ lcs k N₂

Tactic:
induction k with
| zero => simp
| succ k ih => simp only [LieSubmodule.lcs_succ, ih, LieSubmodule.lie_sup]

Result:
no goals

Proof state:
case succ
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N₁ N₂ : LieSubmodule R L M
k : ℕ
ih : lcs k (N₁ ⊔ N₂) = lcs k N₁ ⊔ lcs k N₂
⊢ lcs (k + 1) (N₁ ⊔ N₂) = lcs (k + 1) N₁ ⊔ lcs (k + 1) N₂

Tactic:
simp only [LieSubmodule.lcs_succ, ih, LieSubmodule.lie_sup]

Result:
no goals

Proof state:
case zero
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N₁ N₂ : LieSubmodule R L M
⊢ lcs 0 (N₁ ⊔ N₂) = lcs 0 N₁ ⊔ lcs 0 N₂

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/TwoSidedIdeal/BigOperators.lean
lemma finsetProd_mem {ι : Type*} (s : Finset ι) (f : ι → R) (hs : ∃ x ∈ s, f x ∈ I) :
    s.prod f ∈ I

Proof state:
R : Type u_1
inst✝ : CommRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Finset ι
f : ι → R
hs : ∃ x ∈ s, f x ∈ I
⊢ s.prod f ∈ I

Tactic:
rcases s

Result:
case mk
R : Type u_1
inst✝ : CommRing R
I : TwoSidedIdeal R
ι : Type u_2
f : ι → R
val✝ : Multiset ι
nodup✝ : val✝.Nodup
hs : ∃ x ∈ { val := val✝, nodup := nodup✝ }, f x ∈ I
⊢ { val := val✝, nodup := nodup✝ }.prod f ∈ I

Proof state:
case mk
R : Type u_1
inst✝ : CommRing R
I : TwoSidedIdeal R
ι : Type u_2
f : ι → R
val✝ : Multiset ι
nodup✝ : val✝.Nodup
hs : ∃ x ∈ { val := val✝, nodup := nodup✝ }, f x ∈ I
⊢ { val := val✝, nodup := nodup✝ }.prod f ∈ I

Tactic:
simpa using multiSetProd_mem (hs := hs)

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem tensorLeftTensor_inv_app (X Y Z : C) :
    (tensorLeftTensor X Y).inv.app Z = (associator X Y Z).inv

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z : C
⊢ (tensorLeftTensor X Y).inv.app Z = (α_ X Y Z).inv

Tactic:
simp [tensorLeftTensor]

Result:
no goals
-- Mathlib/RingTheory/Localization/Away/Basic.lean
lemma away_of_isIdempotentElem {R S} [CommRing R] [CommRing S] [Algebra R S]
    {e : R} (he : IsIdempotentElem e)
    (H : RingHom.ker (algebraMap R S) = Ideal.span {1 - e})
    (H' : Function.Surjective (algebraMap R S)) :
    IsLocalization.Away e S :=
  away_of_isIdempotentElem_of_mul he (fun x y ↦ by
    rw [← sub_eq_zero, ← map_sub, ← RingHom.mem_ker, H, ← he.ker_toSpanSingleton_eq_span,
      LinearMap.mem_ker, LinearMap.toSpanSingleton_apply, sub_smul, sub_eq_zero]
    simp_rw [mul_comm e, smul_eq_mul]) H'

Proof state:
R : Type u_4
S : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
e : R
he : IsIdempotentElem e
H : RingHom.ker (algebraMap R S) = Ideal.span {1 - e}
H' : Function.Surjective ⇑(algebraMap R S)
x y : R
⊢ (algebraMap R S) x = (algebraMap R S) y ↔ e * x = e * y

Tactic:
rw [← sub_eq_zero, ← map_sub, ← RingHom.mem_ker, H, ← he.ker_toSpanSingleton_eq_span,
  LinearMap.mem_ker, LinearMap.toSpanSingleton_apply, sub_smul, sub_eq_zero]

Result:
R : Type u_4
S : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
e : R
he : IsIdempotentElem e
H : RingHom.ker (algebraMap R S) = Ideal.span {1 - e}
H' : Function.Surjective ⇑(algebraMap R S)
x y : R
⊢ x • e = y • e ↔ e * x = e * y

Proof state:
R : Type u_4
S : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
e : R
he : IsIdempotentElem e
H : RingHom.ker (algebraMap R S) = Ideal.span {1 - e}
H' : Function.Surjective ⇑(algebraMap R S)
x y : R
⊢ x • e = y • e ↔ e * x = e * y

Tactic:
simp_rw [mul_comm e, smul_eq_mul]

Result:
no goals
-- Mathlib/Algebra/Tropical/Basic.lean
theorem succ_nsmul {R} [LinearOrder R] [OrderTop R] (x : Tropical R) (n : ℕ) : (n + 1) • x = x

Proof state:
case succ
R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
x : Tropical R
n : ℕ
IH : (n + 1) • x = x
⊢ (n + 1 + 1) • x = x

Tactic:
rw [add_nsmul, IH, one_nsmul, add_self]

Result:
no goals

Proof state:
case zero
R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
x : Tropical R
⊢ (0 + 1) • x = x

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
x : Tropical R
n : ℕ
⊢ (n + 1) • x = x

Tactic:
induction n with
| zero => simp
| succ n IH => rw [add_nsmul, IH, one_nsmul, add_self]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Ring.lean
theorem hasSum_mul_right_iff (h : a₂ ≠ 0) : HasSum (fun i ↦ f i * a₂) (a₁ * a₂) ↔ HasSum f a₁ :=
  ⟨fun H ↦ by simpa only [mul_inv_cancel_right₀ h] using H.mul_right a₂⁻¹, HasSum.mul_right _⟩

Proof state:
ι : Type u_1
α : Type u_3
inst✝² : DivisionSemiring α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalSemiring α
f : ι → α
a₁ a₂ : α
h : a₂ ≠ 0
H : HasSum (fun i => f i * a₂) (a₁ * a₂)
⊢ HasSum f a₁

Tactic:
simpa only [mul_inv_cancel_right₀ h] using H.mul_right a₂⁻¹

Result:
no goals
-- Mathlib/RingTheory/RingHomProperties.lean
/-- Variant of `MorphismProperty.arrow_mk_iso_iff` specialized to morphism properties in
`CommRingCat` given by ring hom properties. -/
lemma RespectsIso.arrow_mk_iso_iff (hQ : RingHom.RespectsIso P) {A B A' B' : CommRingCat}
    {f : A ⟶ B} {g : A' ⟶ B'} (e : Arrow.mk f ≅ Arrow.mk g) :
    P f.hom ↔ P g.hom

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
A B A' B' : CommRingCat
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
⊢ P (CommRingCat.Hom.hom f) ↔ P (CommRingCat.Hom.hom g)

Tactic:
have : (toMorphismProperty P).RespectsIso := by
  rwa [← toMorphismProperty_respectsIso_iff]

Result:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
A B A' B' : CommRingCat
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
this : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] => P).RespectsIso
⊢ P (CommRingCat.Hom.hom f) ↔ P (CommRingCat.Hom.hom g)

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
A B A' B' : CommRingCat
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
⊢ (toMorphismProperty fun {R S} [CommRing R] [CommRing S] => P).RespectsIso

Tactic:
rwa [← toMorphismProperty_respectsIso_iff]

Result:
no goals

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
A B A' B' : CommRingCat
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
this : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] => P).RespectsIso
⊢ P (CommRingCat.Hom.hom f) ↔ P (CommRingCat.Hom.hom g)

Tactic:
change toMorphismProperty P _ ↔ toMorphismProperty P _

Result:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
A B A' B' : CommRingCat
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
this : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] => P).RespectsIso
⊢ toMorphismProperty (fun {R S} [CommRing R] [CommRing S] => P) f ↔
    toMorphismProperty (fun {R S} [CommRing R] [CommRing S] => P) g

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
A B A' B' : CommRingCat
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
this : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] => P).RespectsIso
⊢ toMorphismProperty (fun {R S} [CommRing R] [CommRing S] => P) f ↔
    toMorphismProperty (fun {R S} [CommRing R] [CommRing S] => P) g

Tactic:
rw [MorphismProperty.arrow_mk_iso_iff (toMorphismProperty P) e]

Result:
no goals
-- Mathlib/ModelTheory/FinitelyGenerated.lean
theorem fg_def {N : L.Substructure M} : N.FG ↔ ∃ S : Set M, S.Finite ∧ closure L S = N :=
  ⟨fun ⟨t, h⟩ => ⟨_, Finset.finite_toSet t, h⟩, by
    rintro ⟨t', h, rfl⟩
    rcases Finite.exists_finset_coe h with ⟨t, rfl⟩
    exact ⟨t, rfl⟩⟩

Proof state:
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
⊢ (∃ S, S.Finite ∧ (closure L).toFun S = N) → N.FG

Tactic:
rintro ⟨t', h, rfl⟩

Result:
case intro.intro
L : Language
M : Type u_1
inst✝ : L.Structure M
t' : Set M
h : t'.Finite
⊢ ((closure L).toFun t').FG

Proof state:
case intro.intro
L : Language
M : Type u_1
inst✝ : L.Structure M
t' : Set M
h : t'.Finite
⊢ ((closure L).toFun t').FG

Tactic:
rcases Finite.exists_finset_coe h with ⟨t, rfl⟩

Result:
case intro.intro.intro
L : Language
M : Type u_1
inst✝ : L.Structure M
t : Finset M
h : (↑t).Finite
⊢ ((closure L).toFun ↑t).FG

Proof state:
case intro.intro.intro
L : Language
M : Type u_1
inst✝ : L.Structure M
t : Finset M
h : (↑t).Finite
⊢ ((closure L).toFun ↑t).FG

Tactic:
exact ⟨t, rfl⟩

Result:
no goals