harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean
theorem normalizedFactors_irreducible {a : α} (ha : Irreducible a) :
    normalizedFactors a = {normalize a}

Proof state:
case intro.intro
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
p : α
a_assoc : a ~ᵤ p
hp : normalizedFactors a = {p}
p_mem : p ∈ normalizedFactors a
⊢ normalizedFactors a = {normalize a}

Tactic:
convert hp

Result:
case h.e'_3.h.e'_4
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
p : α
a_assoc : a ~ᵤ p
hp : normalizedFactors a = {p}
p_mem : p ∈ normalizedFactors a
⊢ normalize a = p

Proof state:
case intro.intro
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
p : α
a_assoc : a ~ᵤ p
hp : normalizedFactors a = {p}
⊢ normalizedFactors a = {normalize a}

Tactic:
have p_mem : p ∈ normalizedFactors a := by
  rw [hp]
  exact Multiset.mem_singleton_self _

Result:
case intro.intro
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
p : α
a_assoc : a ~ᵤ p
hp : normalizedFactors a = {p}
p_mem : p ∈ normalizedFactors a
⊢ normalizedFactors a = {normalize a}

Proof state:
case h.e'_3.h.e'_4
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
p : α
a_assoc : a ~ᵤ p
hp : normalizedFactors a = {p}
p_mem : p ∈ normalizedFactors a
⊢ normalize a = p

Tactic:
rwa [← normalize_normalized_factor p p_mem, normalize_eq_normalize_iff, dvd_dvd_iff_associated]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
p : α
a_assoc : a ~ᵤ p
hp : normalizedFactors a = {p}
⊢ p ∈ normalizedFactors a

Tactic:
rw [hp]

Result:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
p : α
a_assoc : a ~ᵤ p
hp : normalizedFactors a = {p}
⊢ p ∈ {p}

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
p : α
a_assoc : a ~ᵤ p
hp : normalizedFactors a = {p}
⊢ p ∈ {p}

Tactic:
exact Multiset.mem_singleton_self _

Result:
no goals

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
⊢ normalizedFactors a = {normalize a}

Tactic:
obtain ⟨p, a_assoc, hp⟩ :=
  prime_factors_irreducible ha ⟨prime_of_normalized_factor, prod_normalizedFactors ha.ne_zero⟩

Result:
case intro.intro
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
p : α
a_assoc : a ~ᵤ p
hp : normalizedFactors a = {p}
⊢ normalizedFactors a = {normalize a}
-- Mathlib/Logic/Equiv/Fintype.lean
theorem Equiv.Perm.viaFintypeEmbedding_apply_mem_range {b : β} (h : b ∈ Set.range f) :
    e.viaFintypeEmbedding f b = f (e (f.invOfMemRange ⟨b, h⟩))

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
e : Perm α
f : α ↪ β
b : β
h : b ∈ Set.range ⇑f
⊢ (e.viaFintypeEmbedding f) b = f (e (f.invOfMemRange ⟨b, h⟩))

Tactic:
simp only [viaFintypeEmbedding, Function.Embedding.invOfMemRange]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
e : Perm α
f : α ↪ β
b : β
h : b ∈ Set.range ⇑f
⊢ (e.extendDomain f.toEquivRange) b = f (e (⋯.invOfMemRange ⟨b, h⟩))

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
e : Perm α
f : α ↪ β
b : β
h : b ∈ Set.range ⇑f
⊢ (e.extendDomain f.toEquivRange) b = f (e (⋯.invOfMemRange ⟨b, h⟩))

Tactic:
rw [Equiv.Perm.extendDomain_apply_subtype]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
e : Perm α
f : α ↪ β
b : β
h : b ∈ Set.range ⇑f
⊢ ↑(f.toEquivRange (e (f.toEquivRange.symm ⟨b, ?h⟩))) = f (e (⋯.invOfMemRange ⟨b, h⟩))

case h
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
e : Perm α
f : α ↪ β
b : β
h : b ∈ Set.range ⇑f
⊢ b ∈ Set.range ⇑f

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
e : Perm α
f : α ↪ β
b : β
h : b ∈ Set.range ⇑f
⊢ ↑(f.toEquivRange (e (f.toEquivRange.symm ⟨b, ?h⟩))) = f (e (⋯.invOfMemRange ⟨b, h⟩))

case h
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
e : Perm α
f : α ↪ β
b : β
h : b ∈ Set.range ⇑f
⊢ b ∈ Set.range ⇑f

Tactic:
congr

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
lemma isIdempotentElemEquivClopens_symm_sup (s₁ s₂ : Clopens (PrimeSpectrum R)) :
    letI e := isIdempotentElemEquivClopens (R := R).symm
    e (s₁ ⊔ s₂) = ⟨_, (e s₁).2.add_sub_mul (e s₂).2⟩ := Subtype.ext <| by
  rw [← compl_compl (_ ⊔ _), compl_sup, isIdempotentElemEquivClopens_symm_compl]
  simp_rw [isIdempotentElemEquivClopens_symm_inf, isIdempotentElemEquivClopens_symm_compl]
  ring

Proof state:
R : Type u
inst✝ : CommRing R
s₁ s₂ : Clopens (PrimeSpectrum R)
⊢ ↑(isIdempotentElemEquivClopens.symm (s₁ ⊔ s₂)) =
    ↑⟨↑(isIdempotentElemEquivClopens.symm s₁) + ↑(isIdempotentElemEquivClopens.symm s₂) -
          ↑(isIdempotentElemEquivClopens.symm s₁) * ↑(isIdempotentElemEquivClopens.symm s₂),
        ⋯⟩

Tactic:
rw [← compl_compl (_ ⊔ _), compl_sup, isIdempotentElemEquivClopens_symm_compl]

Result:
R : Type u
inst✝ : CommRing R
s₁ s₂ : Clopens (PrimeSpectrum R)
⊢ ↑⟨1 - ↑(isIdempotentElemEquivClopens.symm (s₁ᶜ ⊓ s₂ᶜ)), ⋯⟩ =
    ↑⟨↑(isIdempotentElemEquivClopens.symm s₁) + ↑(isIdempotentElemEquivClopens.symm s₂) -
          ↑(isIdempotentElemEquivClopens.symm s₁) * ↑(isIdempotentElemEquivClopens.symm s₂),
        ⋯⟩

Proof state:
R : Type u
inst✝ : CommRing R
s₁ s₂ : Clopens (PrimeSpectrum R)
⊢ 1 - (1 - ↑(isIdempotentElemEquivClopens.symm s₁)) * (1 - ↑(isIdempotentElemEquivClopens.symm s₂)) =
    ↑(isIdempotentElemEquivClopens.symm s₁) + ↑(isIdempotentElemEquivClopens.symm s₂) -
      ↑(isIdempotentElemEquivClopens.symm s₁) * ↑(isIdempotentElemEquivClopens.symm s₂)

Tactic:
ring

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
s₁ s₂ : Clopens (PrimeSpectrum R)
⊢ ↑⟨1 - ↑(isIdempotentElemEquivClopens.symm (s₁ᶜ ⊓ s₂ᶜ)), ⋯⟩ =
    ↑⟨↑(isIdempotentElemEquivClopens.symm s₁) + ↑(isIdempotentElemEquivClopens.symm s₂) -
          ↑(isIdempotentElemEquivClopens.symm s₁) * ↑(isIdempotentElemEquivClopens.symm s₂),
        ⋯⟩

Tactic:
simp_rw [isIdempotentElemEquivClopens_symm_inf, isIdempotentElemEquivClopens_symm_compl]

Result:
R : Type u
inst✝ : CommRing R
s₁ s₂ : Clopens (PrimeSpectrum R)
⊢ 1 - (1 - ↑(isIdempotentElemEquivClopens.symm s₁)) * (1 - ↑(isIdempotentElemEquivClopens.symm s₂)) =
    ↑(isIdempotentElemEquivClopens.symm s₁) + ↑(isIdempotentElemEquivClopens.symm s₂) -
      ↑(isIdempotentElemEquivClopens.symm s₁) * ↑(isIdempotentElemEquivClopens.symm s₂)
-- Mathlib/Analysis/Complex/ReImTopology.lean
theorem closure_setOf_re_lt (a : ℝ) : closure { z : ℂ | z.re < a } = { z | z.re ≤ a }

Proof state:
a : ℝ
⊢ closure {z | z.re < a} = {z | z.re ≤ a}

Tactic:
simpa only [closure_Iio] using closure_preimage_re (Iio a)

Result:
no goals
-- Mathlib/Analysis/Asymptotics/ExpGrowth.lean
lemma expGrowthSup_add {u v : ℕ → ℝ≥0∞} :
    expGrowthSup (u + v) = expGrowthSup u ⊔ expGrowthSup v

Proof state:
case a
u v : ℕ → ℝ≥0∞
⊢ expGrowthSup (u + v) ≤ expGrowthSup (u ⊔ v)

Tactic:
refine expGrowthSup_le_of_eventually_le (C := 2) ofNat_ne_top (Eventually.of_forall fun n ↦ ?_)

Result:
case a
u v : ℕ → ℝ≥0∞
n : ℕ
⊢ (u + v) n ≤ 2 * (u ⊔ v) n

Proof state:
case a
u v : ℕ → ℝ≥0∞
n : ℕ
⊢ (u ⊔ v) n ≤ (u + v) n

Tactic:
rw [Pi.sup_apply u v n, Pi.add_apply u v n]

Result:
case a
u v : ℕ → ℝ≥0∞
n : ℕ
⊢ u n ⊔ v n ≤ u n + v n

Proof state:
case a
u v : ℕ → ℝ≥0∞
n : ℕ
⊢ u n + v n ≤ u n ⊔ v n + u n ⊔ v n

Tactic:
exact add_le_add (le_max_left (u n) (v n)) (le_max_right (u n) (v n))

Result:
no goals

Proof state:
case a
u v : ℕ → ℝ≥0∞
n : ℕ
⊢ u n ⊔ v n ≤ u n + v n

Tactic:
exact sup_le (self_le_add_right (u n) (v n)) (self_le_add_left (v n) (u n))

Result:
no goals

Proof state:
case a
u v : ℕ → ℝ≥0∞
n : ℕ
⊢ (u + v) n ≤ 2 * (u ⊔ v) n

Tactic:
rw [Pi.sup_apply u v n, Pi.add_apply u v n, two_mul]

Result:
case a
u v : ℕ → ℝ≥0∞
n : ℕ
⊢ u n + v n ≤ u n ⊔ v n + u n ⊔ v n

Proof state:
case a
u v : ℕ → ℝ≥0∞
⊢ expGrowthSup (u ⊔ v) ≤ expGrowthSup (u + v)

Tactic:
refine expGrowthSup_monotone fun n ↦ ?_

Result:
case a
u v : ℕ → ℝ≥0∞
n : ℕ
⊢ (u ⊔ v) n ≤ (u + v) n

Proof state:
u v : ℕ → ℝ≥0∞
⊢ expGrowthSup (u + v) = expGrowthSup (u ⊔ v)

Tactic:
apply le_antisymm

Result:
case a
u v : ℕ → ℝ≥0∞
⊢ expGrowthSup (u + v) ≤ expGrowthSup (u ⊔ v)

case a
u v : ℕ → ℝ≥0∞
⊢ expGrowthSup (u ⊔ v) ≤ expGrowthSup (u + v)

Proof state:
u v : ℕ → ℝ≥0∞
⊢ expGrowthSup (u + v) = expGrowthSup u ⊔ expGrowthSup v

Tactic:
rw [← expGrowthSup_sup]

Result:
u v : ℕ → ℝ≥0∞
⊢ expGrowthSup (u + v) = expGrowthSup (u ⊔ v)
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem sUnion_apply {x : Class} {y : ZFSet} : (⋃₀ x) y ↔ ∃ z : ZFSet, x z ∧ y ∈ z

Proof state:
x : Class.{u_1}
y : ZFSet.{u_1}
⊢ (⋃₀ x) y ↔ ∃ z, x z ∧ y ∈ z

Tactic:
constructor

Result:
case mp
x : Class.{u_1}
y : ZFSet.{u_1}
⊢ (⋃₀ x) y → ∃ z, x z ∧ y ∈ z

case mpr
x : Class.{u_1}
y : ZFSet.{u_1}
⊢ (∃ z, x z ∧ y ∈ z) → (⋃₀ x) y

Proof state:
case mp
x : Class.{u_1}
y : ZFSet.{u_1}
⊢ (⋃₀ x) y → ∃ z, x z ∧ y ∈ z

Tactic:
rintro ⟨-, ⟨z, rfl, hxz⟩, hyz⟩

Result:
case mp.intro.intro.intro.intro
x : Class.{u_1}
y z : ZFSet.{u_1}
hxz : x z
hyz : y ∈ ↑z
⊢ ∃ z, x z ∧ y ∈ z

Proof state:
case mpr
x : Class.{u_1}
y : ZFSet.{u_1}
⊢ (∃ z, x z ∧ y ∈ z) → (⋃₀ x) y

Tactic:
exact fun ⟨z, hxz, hyz⟩ => ⟨_, coe_mem.2 hxz, hyz⟩

Result:
no goals

Proof state:
case mp.intro.intro.intro.intro
x : Class.{u_1}
y z : ZFSet.{u_1}
hxz : x z
hyz : y ∈ ↑z
⊢ ∃ z, x z ∧ y ∈ z

Tactic:
exact ⟨z, hxz, hyz⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Linear.lean
theorem ExprCnstr.eq_of_toNormPoly_eq (ctx : Context) (c d : ExprCnstr) (h : c.toNormPoly == d.toPoly) : c.denote ctx = d.denote ctx

Proof state:
ctx : Context
c d : ExprCnstr
h✝ : (c.toNormPoly == d.toPoly) = true
h : denote ctx c = denote ctx d
⊢ denote ctx c = denote ctx d

Tactic:
assumption

Result:
no goals

Proof state:
ctx : Context
c d : ExprCnstr
h : (c.toNormPoly == d.toPoly) = true
⊢ denote ctx c = denote ctx d

Tactic:
have h := congrArg (PolyCnstr.denote ctx) (eq_of_beq h)

Result:
ctx : Context
c d : ExprCnstr
h✝ : (c.toNormPoly == d.toPoly) = true
h : PolyCnstr.denote ctx c.toNormPoly = PolyCnstr.denote ctx d.toPoly
⊢ denote ctx c = denote ctx d

Proof state:
ctx : Context
c d : ExprCnstr
h✝ : (c.toNormPoly == d.toPoly) = true
h : PolyCnstr.denote ctx c.toNormPoly = PolyCnstr.denote ctx d.toPoly
⊢ denote ctx c = denote ctx d

Tactic:
simp [-eq_iff_iff] at h

Result:
ctx : Context
c d : ExprCnstr
h✝ : (c.toNormPoly == d.toPoly) = true
h : denote ctx c = denote ctx d
⊢ denote ctx c = denote ctx d
-- Mathlib/Analysis/Convex/Jensen.lean
/-- If a function `f` is convex on `s`, then the value it takes at some center of mass of points of
`s` is less than the value it takes on one of those points. -/
lemma ConvexOn.exists_ge_of_centerMass {t : Finset ι} (h : ConvexOn 𝕜 s f)
    (hw₀ : ∀ i ∈ t, 0 ≤ w i) (hw₁ : 0 < ∑ i ∈ t, w i) (hp : ∀ i ∈ t, p i ∈ s) :
    ∃ i ∈ t, f (t.centerMass w p) ≤ f (p i)

Proof state:
case intro.intro
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
t : Finset ι
h : ConvexOn 𝕜 s f
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : 0 < ∑ i ∈ t, w i
hp : ∀ i ∈ t, p i ∈ s
y : E := t.centerMass w p
i : ι
hi : i ∈ t ∧ w i ≠ 0
hfi : w i • f y ≤ w i • (f ∘ p) i
⊢ ∃ i ∈ t, f y ≤ f (p i)

Tactic:
exact ⟨i, hi.1, (smul_le_smul_iff_of_pos_left <| (hw₀ i hi.1).lt_of_ne hi.2.symm).1 hfi⟩

Result:
no goals
-- Mathlib/Data/Finite/Prod.lean
theorem Finite.prod (hs : s.Finite) (ht : t.Finite) : (s ×ˢ t : Set (α × β)).Finite

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
hs : s.Finite
ht : t.Finite
this : Finite ↑s
⊢ (s ×ˢ t).Finite

Tactic:
have := ht.to_subtype

Result:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
hs : s.Finite
ht : t.Finite
this✝ : Finite ↑s
this : Finite ↑t
⊢ (s ×ˢ t).Finite

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
hs : s.Finite
ht : t.Finite
this✝ : Finite ↑s
this : Finite ↑t
⊢ (s ×ˢ t).Finite

Tactic:
apply toFinite

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
hs : s.Finite
ht : t.Finite
⊢ (s ×ˢ t).Finite

Tactic:
have := hs.to_subtype

Result:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
hs : s.Finite
ht : t.Finite
this : Finite ↑s
⊢ (s ×ˢ t).Finite
-- Mathlib/Algebra/Order/Group/MinMax.lean
theorem min_div_div_left' (a b c : α) : min (a / b) (a / c) = a / max b c

Proof state:
α : Type u_1
inst✝ : LinearOrderedCommGroup α
a b c : α
⊢ a / b ⊓ a / c = a / (b ⊔ c)

Tactic:
simp only [div_eq_mul_inv, min_mul_mul_left, min_inv_inv']

Result:
no goals
-- Mathlib/CategoryTheory/Equivalence.lean
theorem fun_inv_map (F : C ⥤ D) [IsEquivalence F] (X Y : D) (f : X ⟶ Y) :
    F.map (F.inv.map f) = F.asEquivalence.counit.app X ≫ f ≫ F.asEquivalence.counitInv.app Y

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.IsEquivalence
X Y : D
f : X ⟶ Y
⊢ F.map (F.inv.map f) = (F.asEquivalence.inverse ⋙ F.asEquivalence.functor).map f

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.IsEquivalence
X Y : D
f : X ⟶ Y
⊢ F.map (F.inv.map f) = F.asEquivalence.counit.app X ≫ f ≫ F.asEquivalence.counitInv.app Y

Tactic:
erw [NatIso.naturality_2]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.IsEquivalence
X Y : D
f : X ⟶ Y
⊢ F.map (F.inv.map f) = (F.asEquivalence.inverse ⋙ F.asEquivalence.functor).map f
-- Mathlib/Analysis/SpecialFunctions/Exp.lean
lemma summable_exp_neg_nat : Summable fun n : ℕ ↦ exp (-n)

Proof state:
⊢ Summable fun n => rexp (-↑n)

Tactic:
simpa only [mul_neg_one] using summable_exp_nat_mul_iff.mpr neg_one_lt_zero

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem mul_mem_closedBall_mul_iff {c : E} : a * c ∈ closedBall (b * c) r ↔ a ∈ closedBall b r

Proof state:
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
c : E
⊢ a * c ∈ closedBall (b * c) r ↔ a ∈ closedBall b r

Tactic:
simp only [mem_closedBall, dist_eq_norm_div, mul_div_mul_right_eq_div]

Result:
no goals
-- Mathlib/Data/Matrix/RowCol.lean
theorem updateCol_transpose [DecidableEq m] : updateCol Mᵀ i b = (updateRow M i b)ᵀ

Proof state:
case a
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
b : n → α
inst✝ : DecidableEq m
i✝ : n
j✝ : m
⊢ (if j✝ = i then b i✝ else Mᵀ i✝ j✝) = if j✝ = i then b i✝ else M j✝ i✝

Tactic:
rfl

Result:
no goals

Proof state:
case a
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
b : n → α
inst✝ : DecidableEq m
i✝ : n
j✝ : m
⊢ Mᵀ.updateCol i b i✝ j✝ = (M.updateRow i b)ᵀ i✝ j✝

Tactic:
rw [transpose_apply, updateRow_apply, updateCol_apply]

Result:
case a
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
b : n → α
inst✝ : DecidableEq m
i✝ : n
j✝ : m
⊢ (if j✝ = i then b i✝ else Mᵀ i✝ j✝) = if j✝ = i then b i✝ else M j✝ i✝

Proof state:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
b : n → α
inst✝ : DecidableEq m
⊢ Mᵀ.updateCol i b = (M.updateRow i b)ᵀ

Tactic:
ext

Result:
case a
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
b : n → α
inst✝ : DecidableEq m
i✝ : n
j✝ : m
⊢ Mᵀ.updateCol i b i✝ j✝ = (M.updateRow i b)ᵀ i✝ j✝
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem foldl_attachWith
    (l : List α) {q : α → Prop} (H : ∀ a, a ∈ l → q a) {f : β → { x // q x} → β} {b} :
    (l.attachWith q H).foldl f b = l.attach.foldl (fun b ⟨a, h⟩ => f b ⟨a, H _ h⟩) b

Proof state:
case nil
α : Type u_1
β : Type u_2
q : α → Prop
f : β → { x // q x } → β
H : ∀ (a : α), a ∈ [] → q a
b : β
⊢ foldl f b ([].attachWith q H) =
    foldl
      (fun b x =>
        match x with
        | ⟨a, h⟩ => f b ⟨a, ⋯⟩)
      b [].attach

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : List α
q : α → Prop
H : ∀ (a : α), a ∈ l → q a
f : β → { x // q x } → β
b : β
⊢ foldl f b (l.attachWith q H) =
    foldl
      (fun b x =>
        match x with
        | ⟨a, h⟩ => f b ⟨a, ⋯⟩)
      b l.attach

Tactic:
induction l generalizing b with
| nil => simp
| cons a l ih => simp [ih, foldl_map]

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
q : α → Prop
f : β → { x // q x } → β
a : α
l : List α
ih :
  ∀ (H : ∀ (a : α), a ∈ l → q a) {b : β},
    foldl f b (l.attachWith q H) =
      foldl
        (fun b x =>
          match x with
          | ⟨a, h⟩ => f b ⟨a, ⋯⟩)
        b l.attach
H : ∀ (a_1 : α), a_1 ∈ a :: l → q a_1
b : β
⊢ foldl f b ((a :: l).attachWith q H) =
    foldl
      (fun b x =>
        match x with
        | ⟨a_1, h⟩ => f b ⟨a_1, ⋯⟩)
      b (a :: l).attach

Tactic:
simp [ih, foldl_map]

Result:
no goals
-- Mathlib/Topology/UnitInterval.lean
theorem symm_le_comm {i j : I} : σ i ≤ j ↔ σ j ≤ i

Proof state:
i j : ↑I
⊢ σ i ≤ j ↔ σ j ≤ i

Tactic:
rw [← symm_le_symm, symm_symm]

Result:
no goals
-- Mathlib/Analysis/Convex/Segment.lean
theorem image_mk_openSegment_left (x₁ x₂ : E) (y : F) :
    (fun x => (x, y)) '' openSegment 𝕜 x₁ x₂ = openSegment 𝕜 (x₁, y) (x₂, y)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x₁ x₂ : E
y : F
⊢ (fun x => (x, y)) '' openSegment 𝕜 x₁ x₂ = openSegment 𝕜 (x₁, y) (x₂, y)

Tactic:
rw [openSegment_eq_image₂, openSegment_eq_image₂, image_image]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x₁ x₂ : E
y : F
⊢ (fun x => (x.1 • x₁ + x.2 • x₂, y)) '' {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1} =
    (fun p => p.1 • (x₁, y) + p.2 • (x₂, y)) '' {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1}

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x₁ x₂ : E
y : F
⊢ (fun x => (x.1 • x₁ + x.2 • x₂, y)) '' {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1} =
    (fun p => p.1 • (x₁, y) + p.2 • (x₂, y)) '' {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1}

Tactic:
refine EqOn.image_eq fun a ha ↦ ?_

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x₁ x₂ : E
y : F
a : 𝕜 × 𝕜
ha : a ∈ {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1}
⊢ (a.1 • x₁ + a.2 • x₂, y) = a.1 • (x₁, y) + a.2 • (x₂, y)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x₁ x₂ : E
y : F
a : 𝕜 × 𝕜
ha : a ∈ {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1}
⊢ (a.1 • x₁ + a.2 • x₂, y) = a.1 • (x₁, y) + a.2 • (x₂, y)

Tactic:
simp [Convex.combo_self ha.2.2]

Result:
no goals
-- Mathlib/RingTheory/Ideal/MinimalPrime/Localization.lean
/-- minimal primes are contained in zero divisors. -/
lemma Ideal.disjoint_nonZeroDivisors_of_mem_minimalPrimes {p : Ideal R} (hp : p ∈ minimalPrimes R) :
    Disjoint (p : Set R) (nonZeroDivisors R)

Proof state:
R : Type u_1
inst✝ : CommSemiring R
p : Ideal R
hp : p ∈ minimalPrimes R
⊢ Disjoint ↑p ↑(nonZeroDivisors R)

Tactic:
rw [← Set.subset_compl_iff_disjoint_right, Set.subset_def]

Result:
R : Type u_1
inst✝ : CommSemiring R
p : Ideal R
hp : p ∈ minimalPrimes R
⊢ ∀ x ∈ ↑p, x ∈ (↑(nonZeroDivisors R))ᶜ

Proof state:
R : Type u_1
inst✝ : CommSemiring R
p : Ideal R
hp : p ∈ minimalPrimes R
x : R
hxp : x ∈ p
⊢ ∃ x_1, ¬x_1 = 0 ∧ x * x_1 = 0

Tactic:
exact Ideal.exists_mul_mem_of_mem_minimalPrimes hp hxp

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
p : Ideal R
hp : p ∈ minimalPrimes R
⊢ Disjoint ↑p ↑(nonZeroDivisors R)

Tactic:
classical
rw [← Set.subset_compl_iff_disjoint_right, Set.subset_def]
simp only [SetLike.mem_coe, Set.mem_compl_iff, mem_nonZeroDivisors_iff, not_forall,
  Classical.not_imp]
intro x hxp
simp_rw [exists_prop, @and_comm (_ * _ = _), ← mul_comm x]
exact Ideal.exists_mul_mem_of_mem_minimalPrimes hp hxp

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
p : Ideal R
hp : p ∈ minimalPrimes R
x : R
hxp : x ∈ p
⊢ ∃ x_1, ∃ (_ : x_1 * x = 0), ¬x_1 = 0

Tactic:
simp_rw [exists_prop, @and_comm (_ * _ = _), ← mul_comm x]

Result:
R : Type u_1
inst✝ : CommSemiring R
p : Ideal R
hp : p ∈ minimalPrimes R
x : R
hxp : x ∈ p
⊢ ∃ x_1, ¬x_1 = 0 ∧ x * x_1 = 0

Proof state:
R : Type u_1
inst✝ : CommSemiring R
p : Ideal R
hp : p ∈ minimalPrimes R
⊢ ∀ x ∈ ↑p, x ∈ (↑(nonZeroDivisors R))ᶜ

Tactic:
simp only [SetLike.mem_coe, Set.mem_compl_iff, mem_nonZeroDivisors_iff, not_forall,
  Classical.not_imp]

Result:
R : Type u_1
inst✝ : CommSemiring R
p : Ideal R
hp : p ∈ minimalPrimes R
⊢ ∀ x ∈ p, ∃ x_1, ∃ (_ : x_1 * x = 0), ¬x_1 = 0

Proof state:
R : Type u_1
inst✝ : CommSemiring R
p : Ideal R
hp : p ∈ minimalPrimes R
⊢ ∀ x ∈ p, ∃ x_1, ∃ (_ : x_1 * x = 0), ¬x_1 = 0

Tactic:
intro x hxp

Result:
R : Type u_1
inst✝ : CommSemiring R
p : Ideal R
hp : p ∈ minimalPrimes R
x : R
hxp : x ∈ p
⊢ ∃ x_1, ∃ (_ : x_1 * x = 0), ¬x_1 = 0
-- Mathlib/SetTheory/ZFC/Ordinal.lean
theorem _root_.ZFSet.isOrdinal_iff_isTrans :
    x.IsOrdinal ↔ x.IsTransitive ∧ IsTrans _ (Subrel (· ∈ ·) (· ∈ x)) where
  mp h := ⟨h.isTransitive, h.isTrans⟩
  mpr

Proof state:
case intro.mk
x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ :
  ∀ (a b c : { x_1 // x_1 ∈ x }),
    Subrel (fun x1 x2 => x1 ∈ x2) (fun x_1 => x_1 ∈ x) a b →
      Subrel (fun x1 x2 => x1 ∈ x2) (fun x_1 => x_1 ∈ x) b c → Subrel (fun x1 x2 => x1 ∈ x2) (fun x_1 => x_1 ∈ x) a c
⊢ x.IsOrdinal

Tactic:
refine ⟨h₁, fun {y z w} hyz hzw hwx ↦ ?_⟩

Result:
case intro.mk
x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ :
  ∀ (a b c : { x_1 // x_1 ∈ x }),
    Subrel (fun x1 x2 => x1 ∈ x2) (fun x_1 => x_1 ∈ x) a b →
      Subrel (fun x1 x2 => x1 ∈ x2) (fun x_1 => x_1 ∈ x) b c → Subrel (fun x1 x2 => x1 ∈ x2) (fun x_1 => x_1 ∈ x) a c
y z w : ZFSet.{u}
hyz : y ∈ z
hzw : z ∈ w
hwx : w ∈ x
⊢ y ∈ w

Proof state:
case intro.mk
x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ :
  ∀ (a b c : { x_1 // x_1 ∈ x }),
    Subrel (fun x1 x2 => x1 ∈ x2) (fun x_1 => x_1 ∈ x) a b →
      Subrel (fun x1 x2 => x1 ∈ x2) (fun x_1 => x_1 ∈ x) b c → Subrel (fun x1 x2 => x1 ∈ x2) (fun x_1 => x_1 ∈ x) a c
y z w : ZFSet.{u}
hyz : y ∈ z
hzw : z ∈ w
hwx : w ∈ x
⊢ y ∈ w

Tactic:
have hzx := h₁.mem_trans hzw hwx

Result:
case intro.mk
x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ :
  ∀ (a b c : { x_1 // x_1 ∈ x }),
    Subrel (fun x1 x2 => x1 ∈ x2) (fun x_1 => x_1 ∈ x) a b →
      Subrel (fun x1 x2 => x1 ∈ x2) (fun x_1 => x_1 ∈ x) b c → Subrel (fun x1 x2 => x1 ∈ x2) (fun x_1 => x_1 ∈ x) a c
y z w : ZFSet.{u}
hyz : y ∈ z
hzw : z ∈ w
hwx : w ∈ x
hzx : z ∈ x
⊢ y ∈ w

Proof state:
case intro.mk
x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ :
  ∀ (a b c : { x_1 // x_1 ∈ x }),
    Subrel (fun x1 x2 => x1 ∈ x2) (fun x_1 => x_1 ∈ x) a b →
      Subrel (fun x1 x2 => x1 ∈ x2) (fun x_1 => x_1 ∈ x) b c → Subrel (fun x1 x2 => x1 ∈ x2) (fun x_1 => x_1 ∈ x) a c
y z w : ZFSet.{u}
hyz : y ∈ z
hzw : z ∈ w
hwx : w ∈ x
hzx : z ∈ x
⊢ y ∈ w

Tactic:
exact h₂ ⟨y, h₁.mem_trans hyz hzx⟩ ⟨z, hzx⟩ ⟨w, hwx⟩ hyz hzw

Result:
no goals

Proof state:
x : ZFSet.{u}
⊢ x.IsTransitive ∧ IsTrans { x_1 // x_1 ∈ x } (Subrel (fun x1 x2 => x1 ∈ x2) fun x_1 => x_1 ∈ x) → x.IsOrdinal

Tactic:
rintro ⟨h₁, ⟨h₂⟩⟩

Result:
case intro.mk
x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ :
  ∀ (a b c : { x_1 // x_1 ∈ x }),
    Subrel (fun x1 x2 => x1 ∈ x2) (fun x_1 => x_1 ∈ x) a b →
      Subrel (fun x1 x2 => x1 ∈ x2) (fun x_1 => x_1 ∈ x) b c → Subrel (fun x1 x2 => x1 ∈ x2) (fun x_1 => x_1 ∈ x) a c
⊢ x.IsOrdinal