harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/ENNReal/Inv.lean
lemma add_iSup [Nonempty ι] (f : ι → ℝ≥0∞) : a + ⨆ i, f i = ⨆ i, a + f i

Proof state:
case inl
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ≥0∞
⊢ ⊤ + ⨆ i, f i = ⨆ i, ⊤ + f i

Tactic:
simp

Result:
no goals

Proof state:
case inr
ι : Sort u_1
a : ℝ≥0∞
inst✝ : Nonempty ι
f : ι → ℝ≥0∞
ha : a ≠ ⊤
⊢ a + ⨆ i, f i ≤ ⨆ i, a + f i

Tactic:
refine add_le_of_le_tsub_left_of_le (le_iSup_of_le (Classical.arbitrary _) le_self_add) ?_

Result:
case inr
ι : Sort u_1
a : ℝ≥0∞
inst✝ : Nonempty ι
f : ι → ℝ≥0∞
ha : a ≠ ⊤
⊢ ⨆ i, f i ≤ (⨆ i, a + f i) - a

Proof state:
ι : Sort u_1
a : ℝ≥0∞
inst✝ : Nonempty ι
f : ι → ℝ≥0∞
⊢ a + ⨆ i, f i = ⨆ i, a + f i

Tactic:
obtain rfl | ha := eq_or_ne a ∞

Result:
case inl
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ≥0∞
⊢ ⊤ + ⨆ i, f i = ⨆ i, ⊤ + f i

case inr
ι : Sort u_1
a : ℝ≥0∞
inst✝ : Nonempty ι
f : ι → ℝ≥0∞
ha : a ≠ ⊤
⊢ a + ⨆ i, f i = ⨆ i, a + f i

Proof state:
case inr
ι : Sort u_1
a : ℝ≥0∞
inst✝ : Nonempty ι
f : ι → ℝ≥0∞
ha : a ≠ ⊤
⊢ a + ⨆ i, f i = ⨆ i, a + f i

Tactic:
refine le_antisymm ?_ <| iSup_le fun i ↦ add_le_add_left (le_iSup ..) _

Result:
case inr
ι : Sort u_1
a : ℝ≥0∞
inst✝ : Nonempty ι
f : ι → ℝ≥0∞
ha : a ≠ ⊤
⊢ a + ⨆ i, f i ≤ ⨆ i, a + f i
-- Mathlib/FieldTheory/IsAlgClosed/Basic.lean
theorem roots_eq_zero_iff [IsAlgClosed k] {p : k[X]} :
    p.roots = 0 ↔ p = Polynomial.C (p.coeff 0)

Proof state:
case inr.intro
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
p : k[X]
h : p.roots = 0
hd : 0 < p.degree
z : k
hz : z ∈ 0
⊢ p = C (p.coeff 0)

Tactic:
simp at hz

Result:
no goals

Proof state:
case inr.intro
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
p : k[X]
h : p.roots = 0
hd : 0 < p.degree
z : k
hz : p.IsRoot z
⊢ p = C (p.coeff 0)

Tactic:
rw [← mem_roots (ne_zero_of_degree_gt hd), h] at hz

Result:
case inr.intro
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
p : k[X]
h : p.roots = 0
hd : 0 < p.degree
z : k
hz : z ∈ 0
⊢ p = C (p.coeff 0)

Proof state:
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
p : k[X]
h : p.roots = 0
⊢ p = C (p.coeff 0)

Tactic:
rcases le_or_lt (degree p) 0 with hd | hd

Result:
case inl
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
p : k[X]
h : p.roots = 0
hd : p.degree ≤ 0
⊢ p = C (p.coeff 0)

case inr
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
p : k[X]
h : p.roots = 0
hd : 0 < p.degree
⊢ p = C (p.coeff 0)

Proof state:
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
p : k[X]
⊢ p.roots = 0 ↔ p = C (p.coeff 0)

Tactic:
refine ⟨fun h => ?_, fun hp => by rw [hp, roots_C]⟩

Result:
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
p : k[X]
h : p.roots = 0
⊢ p = C (p.coeff 0)

Proof state:
case inr
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
p : k[X]
h : p.roots = 0
hd : 0 < p.degree
⊢ p = C (p.coeff 0)

Tactic:
obtain ⟨z, hz⟩ := IsAlgClosed.exists_root p hd.ne'

Result:
case inr.intro
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
p : k[X]
h : p.roots = 0
hd : 0 < p.degree
z : k
hz : p.IsRoot z
⊢ p = C (p.coeff 0)

Proof state:
case inl
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
p : k[X]
h : p.roots = 0
hd : p.degree ≤ 0
⊢ p = C (p.coeff 0)

Tactic:
exact eq_C_of_degree_le_zero hd

Result:
no goals

Proof state:
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
p : k[X]
hp : p = C (p.coeff 0)
⊢ p.roots = 0

Tactic:
rw [hp, roots_C]

Result:
no goals
-- Mathlib/Algebra/Algebra/Quasispectrum.lean
lemma of_spectrum_eq {a b : A} {f : S → R} (ha : SpectrumRestricts a f)
    (h : spectrum S a = spectrum S b) : SpectrumRestricts b f where
  rightInvOn :=  by
    rw [quasispectrum_eq_spectrum_union_zero, ← h, ← quasispectrum_eq_spectrum_union_zero]
    exact QuasispectrumRestricts.rightInvOn ha
  left_inv := ha.left_inv

Proof state:
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁵ : Semifield R
inst✝⁴ : Semifield S
inst✝³ : Ring A
inst✝² : Algebra R S
inst✝¹ : Algebra R A
inst✝ : Algebra S A
a b : A
f : S → R
ha : SpectrumRestricts a f
h : spectrum S a = spectrum S b
⊢ Set.RightInvOn f (⇑(algebraMap R S)) (quasispectrum S a)

Tactic:
exact QuasispectrumRestricts.rightInvOn ha

Result:
no goals

Proof state:
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁵ : Semifield R
inst✝⁴ : Semifield S
inst✝³ : Ring A
inst✝² : Algebra R S
inst✝¹ : Algebra R A
inst✝ : Algebra S A
a b : A
f : S → R
ha : SpectrumRestricts a f
h : spectrum S a = spectrum S b
⊢ Set.RightInvOn f (⇑(algebraMap R S)) (quasispectrum S b)

Tactic:
rw [quasispectrum_eq_spectrum_union_zero, ← h, ← quasispectrum_eq_spectrum_union_zero]

Result:
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁵ : Semifield R
inst✝⁴ : Semifield S
inst✝³ : Ring A
inst✝² : Algebra R S
inst✝¹ : Algebra R A
inst✝ : Algebra S A
a b : A
f : S → R
ha : SpectrumRestricts a f
h : spectrum S a = spectrum S b
⊢ Set.RightInvOn f (⇑(algebraMap R S)) (quasispectrum S a)
-- Mathlib/NumberTheory/Transcendental/Liouville/LiouvilleNumber.lean
theorem aux_calc (n : ℕ) {m : ℝ} (hm : 2 ≤ m) :
    (1 - 1 / m)⁻¹ * (1 / m ^ (n + 1)!) ≤ 1 / (m ^ n !) ^ n :=
  calc
    (1 - 1 / m)⁻¹ * (1 / m ^ (n + 1)!) ≤ 2 * (1 / m ^ (n + 1)!) :=
      -- the second factors coincide (and are non-negative),
      -- the first factors satisfy the inequality `sub_one_div_inv_le_two`
      mul_le_mul_of_nonneg_right (sub_one_div_inv_le_two hm) (by positivity)
    _ = 2 / m ^ (n + 1)! := mul_one_div 2 _
    _ = 2 / m ^ (n ! * (n + 1)) := (congr_arg (2 / ·) (congr_arg (Pow.pow m) (mul_comm _ _)))
    _ ≤ 1 / m ^ (n ! * n)

Proof state:
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 2 * m ^ (n ! * n) ≤ 1 * m ^ (n ! * (n + 1))

Tactic:
conv_rhs => rw [one_mul, mul_add, pow_add, mul_one, pow_mul, mul_comm, ← pow_mul]

Result:
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 2 * m ^ (n ! * n) ≤ m ^ n ! * m ^ (n ! * n)

Proof state:
case refine_1
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 < m ^ (n ! * n)

case refine_2
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 2 ≤ m ^ n !

n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 < m ^ (n ! * (n + 1))

n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 < m ^ (n ! * n)

Tactic:
any_goals exact pow_pos (zero_lt_two.trans_le hm) _

Result:
case refine_2
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 2 ≤ m ^ n !

Proof state:
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 < m ^ (n ! * n)

Tactic:
exact pow_pos (zero_lt_two.trans_le hm) _

Result:
no goals

Proof state:
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 2 * m ^ (n ! * n) ≤ m ^ n ! * m ^ (n ! * n)

Tactic:
refine (mul_le_mul_right ?_).mpr ?_

Result:
case refine_1
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 < m ^ (n ! * n)

case refine_2
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 2 ≤ m ^ n !

Proof state:
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 2 * m ^ (n ! * n) ≤ 1 * m ^ (n ! * (n + 1))

n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 < m ^ (n ! * (n + 1))

n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 < m ^ (n ! * n)

Tactic:
focus
  conv_rhs => rw [one_mul, mul_add, pow_add, mul_one, pow_mul, mul_comm, ← pow_mul]
  refine (mul_le_mul_right ?_).mpr ?_

Result:
case refine_1
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 < m ^ (n ! * n)

case refine_2
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 2 ≤ m ^ n !

n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 < m ^ (n ! * (n + 1))

n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 < m ^ (n ! * n)

Proof state:
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 2 / m ^ (n ! * (n + 1)) ≤ 1 / m ^ (n ! * n)

Tactic:
apply (div_le_div_iff₀ _ _).mpr

Result:
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 2 * m ^ (n ! * n) ≤ 1 * m ^ (n ! * (n + 1))

n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 < m ^ (n ! * (n + 1))

n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 < m ^ (n ! * n)

Proof state:
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 ≤ 1 / m ^ (n + 1)!

Tactic:
positivity

Result:
no goals

Proof state:
case refine_2
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 2 ≤ m ^ n !

Tactic:
exact _root_.trans (_root_.trans hm (pow_one _).symm.le)
  (pow_right_mono₀ (one_le_two.trans hm) n.factorial_pos)

Result:
no goals
-- Mathlib/CategoryTheory/ChosenFiniteProducts.lean
@[reassoc (attr := simp)]
lemma lift_leftUnitor_hom {X Y : C} (f : X ⟶ 𝟙_ C) (g : X ⟶ Y) :
    lift f g ≫ (λ_ Y).hom = g

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ChosenFiniteProducts C
X Y : C
f : X ⟶ 𝟙_ C
g : X ⟶ Y
⊢ lift f g = g ≫ (λ_ Y).inv

Tactic:
aesop_cat

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ChosenFiniteProducts C
X Y : C
f : X ⟶ 𝟙_ C
g : X ⟶ Y
⊢ lift f g ≫ (λ_ Y).hom = g

Tactic:
rw [← Iso.eq_comp_inv]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ChosenFiniteProducts C
X Y : C
f : X ⟶ 𝟙_ C
g : X ⟶ Y
⊢ lift f g = g ≫ (λ_ Y).inv
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem reverse_push (as : Vector α n) (a : α) :
    (as.push a).reverse = (#v[a] ++ as.reverse).cast (by omega)

Proof state:
α : Type ?u.350844
n : Nat
as : Vector α n
a : α
⊢ 1 + n = n + 1

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
n : Nat
as : Vector α n
a : α
⊢ (as.push a).reverse = Vector.cast ⋯ ({ toArray := #[a], size_toArray := ⋯ } ++ as.reverse)

Tactic:
rcases as with ⟨as, rfl⟩

Result:
case mk
α : Type u_1
a : α
as : Array α
⊢ ({ toArray := as, size_toArray := ⋯ }.push a).reverse =
    Vector.cast ⋯ ({ toArray := #[a], size_toArray := ⋯ } ++ { toArray := as, size_toArray := ⋯ }.reverse)

Proof state:
case mk
α : Type u_1
a : α
as : Array α
⊢ ({ toArray := as, size_toArray := ⋯ }.push a).reverse =
    Vector.cast ⋯ ({ toArray := #[a], size_toArray := ⋯ } ++ { toArray := as, size_toArray := ⋯ }.reverse)

Tactic:
simp [Array.reverse_push]

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/OfFunction.lean
theorem map_biInf_comap {ι β} {I : Set ι} (hI : I.Nonempty) {f : α → β} (m : ι → OuterMeasure β) :
    map f (⨅ i ∈ I, comap f (m i)) = ⨅ i ∈ I, map f (comap f (m i))

Proof state:
α : Type u_1
ι : Type u_2
β : Type u_3
I : Set ι
hI : I.Nonempty
f : α → β
m : ι → OuterMeasure β
this : Nonempty ↑I
⊢ (map f) (⨅ i ∈ I, (comap f) (m i)) = ⨅ i ∈ I, (map f) ((comap f) (m i))

Tactic:
rw [← iInf_subtype'', ← iInf_subtype'']

Result:
α : Type u_1
ι : Type u_2
β : Type u_3
I : Set ι
hI : I.Nonempty
f : α → β
m : ι → OuterMeasure β
this : Nonempty ↑I
⊢ (map f) (⨅ i, (comap f) (m ↑i)) = ⨅ i, (map f) ((comap f) (m ↑i))

Proof state:
α : Type u_1
ι : Type u_2
β : Type u_3
I : Set ι
hI : I.Nonempty
f : α → β
m : ι → OuterMeasure β
this : Nonempty ↑I
⊢ (map f) (⨅ i, (comap f) (m ↑i)) = ⨅ i, (map f) ((comap f) (m ↑i))

Tactic:
exact map_iInf_comap _

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
β : Type u_3
I : Set ι
hI : I.Nonempty
f : α → β
m : ι → OuterMeasure β
⊢ (map f) (⨅ i ∈ I, (comap f) (m i)) = ⨅ i ∈ I, (map f) ((comap f) (m i))

Tactic:
haveI := hI.to_subtype

Result:
α : Type u_1
ι : Type u_2
β : Type u_3
I : Set ι
hI : I.Nonempty
f : α → β
m : ι → OuterMeasure β
this : Nonempty ↑I
⊢ (map f) (⨅ i ∈ I, (comap f) (m i)) = ⨅ i ∈ I, (map f) ((comap f) (m i))
-- Mathlib/Analysis/Normed/Algebra/MatrixExponential.lean
theorem exp_conj (U : Matrix m m 𝔸) (A : Matrix m m 𝔸) (hy : IsUnit U) :
    exp 𝕂 (U * A * U⁻¹) = U * exp 𝕂 A * U⁻¹ :=
  let ⟨u, hu⟩ := hy
  hu ▸ by simpa only [Matrix.coe_units_inv] using exp_units_conj 𝕂 u A

Proof state:
𝕂 : Type u_1
m : Type u_2
𝔸 : Type u_5
inst✝⁵ : RCLike 𝕂
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NormedCommRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
U A : Matrix m m 𝔸
hy : IsUnit U
u : (Matrix m m 𝔸)ˣ
hu : ↑u = U
⊢ exp 𝕂 (↑u * A * (↑u)⁻¹) = ↑u * exp 𝕂 A * (↑u)⁻¹

Tactic:
simpa only [Matrix.coe_units_inv] using exp_units_conj 𝕂 u A

Result:
no goals
-- Mathlib/MeasureTheory/Function/AEEqFun.lean
theorem toGerm_injective : Injective (toGerm : (α →ₘ[μ] β) → Germ (ae μ) β) := fun f g H =>
  ext <| Germ.coe_eq.1 <| by rwa [← toGerm_eq, ← toGerm_eq]

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
f g : α →ₘ[μ] β
H : f.toGerm = g.toGerm
⊢ ↑↑f = ↑↑g

Tactic:
rwa [← toGerm_eq, ← toGerm_eq]

Result:
no goals
-- Mathlib/RingTheory/RootsOfUnity/Basic.lean
theorem rootsOfUnity_one (M : Type*) [CommMonoid M] : rootsOfUnity 1 M = ⊥

Proof state:
M : Type u_7
inst✝ : CommMonoid M
⊢ rootsOfUnity 1 M = ⊥

Tactic:
ext1

Result:
case h
M : Type u_7
inst✝ : CommMonoid M
x✝ : Mˣ
⊢ x✝ ∈ rootsOfUnity 1 M ↔ x✝ ∈ ⊥

Proof state:
case h
M : Type u_7
inst✝ : CommMonoid M
x✝ : Mˣ
⊢ x✝ ∈ rootsOfUnity 1 M ↔ x✝ ∈ ⊥

Tactic:
simp only [mem_rootsOfUnity, pow_one, Subgroup.mem_bot]

Result:
no goals
-- Mathlib/RingTheory/Valuation/Quotient.lean
theorem comap_onQuot_eq (J : Ideal R) (v : Valuation (R ⧸ J) Γ₀) :
    (v.comap (Ideal.Quotient.mk J)).onQuot (v.self_le_supp_comap J) = v :=
  ext <| by
    rintro ⟨x⟩
    rfl

Proof state:
case mk
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
J : Ideal R
v : Valuation (R ⧸ J) Γ₀
r✝ : R ⧸ J
x : R
⊢ ((comap (Ideal.Quotient.mk J) v).onQuot ⋯) (Quot.mk (⇑(Submodule.quotientRel J)) x) =
    v (Quot.mk (⇑(Submodule.quotientRel J)) x)

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
J : Ideal R
v : Valuation (R ⧸ J) Γ₀
⊢ ∀ (r : R ⧸ J), ((comap (Ideal.Quotient.mk J) v).onQuot ⋯) r = v r

Tactic:
rintro ⟨x⟩

Result:
case mk
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
J : Ideal R
v : Valuation (R ⧸ J) Γ₀
r✝ : R ⧸ J
x : R
⊢ ((comap (Ideal.Quotient.mk J) v).onQuot ⋯) (Quot.mk (⇑(Submodule.quotientRel J)) x) =
    v (Quot.mk (⇑(Submodule.quotientRel J)) x)
-- Mathlib/Combinatorics/SimpleGraph/ConcreteColorings.lean
theorem Coloring.odd_length_iff_not_congr {α} {G : SimpleGraph α}
    (c : G.Coloring Bool) {u v : α} (p : G.Walk u v) :
    Odd p.length ↔ (¬c u ↔ c v)

Proof state:
α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u v : α
p : G.Walk u v
⊢ Odd p.length ↔ (¬c u = true ↔ c v = true)

Tactic:
rw [← Nat.not_even_iff_odd, c.even_length_iff_congr p]

Result:
α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u v : α
p : G.Walk u v
⊢ ¬(c u = true ↔ c v = true) ↔ (¬c u = true ↔ c v = true)

Proof state:
α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u v : α
p : G.Walk u v
⊢ ¬(c u = true ↔ c v = true) ↔ (¬c u = true ↔ c v = true)

Tactic:
tauto

Result:
no goals
-- Mathlib/Analysis/Normed/Group/SemiNormedGrp/Kernels.lean
theorem explicitCokernelπ_desc_apply {X Y Z : SemiNormedGrp.{u}} {f : X ⟶ Y} {g : Y ⟶ Z}
    {cond : f ≫ g = 0} (x : Y) : explicitCokernelDesc cond (explicitCokernelπ f x) = g x :=
  show (explicitCokernelπ f ≫ explicitCokernelDesc cond) x = g x by rw [explicitCokernelπ_desc]

Proof state:
X Y Z : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
cond : f ≫ g = 0
x : Y.carrier
⊢ (ConcreteCategory.hom (explicitCokernelπ f ≫ explicitCokernelDesc cond)) x = (ConcreteCategory.hom g) x

Tactic:
rw [explicitCokernelπ_desc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Monadic.lean
theorem foldlM_attachWith [Monad m]
    (l : List α) {q : α → Prop} (H : ∀ a, a ∈ l → q a) {f : β → { x // q x} → m β} {b} :
    (l.attachWith q H).foldlM f b = l.attach.foldlM (fun b ⟨a, h⟩ => f b ⟨a, H _ h⟩) b

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

Tactic:
simp

Result:
no goals

Proof state:
case cons
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
q : α → Prop
f : β → { x // q x } → m β
a : α
l : List α
ih :
  ∀ (H : ∀ (a : α), a ∈ l → q a) {b : β},
    List.foldlM f b (l.attachWith q H) =
      List.foldlM
        (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 : β
⊢ List.foldlM f b ((a :: l).attachWith q H) =
    List.foldlM
      (fun b x =>
        match x with
        | ⟨a_1, h⟩ => f b ⟨a_1, ⋯⟩)
      b (a :: l).attach

Tactic:
simp [ih, foldlM_map]

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
l : List α
q : α → Prop
H : ∀ (a : α), a ∈ l → q a
f : β → { x // q x } → m β
b : β
⊢ List.foldlM f b (l.attachWith q H) =
    List.foldlM
      (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, foldlM_map]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem support_neg {p : R[X]} : (-p).support = p.support

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
⊢ (-p).support = p.support

Tactic:
rcases p with ⟨⟩

Result:
case ofFinsupp
R : Type u
inst✝ : Ring R
toFinsupp✝ : R[ℕ]
⊢ (-{ toFinsupp := toFinsupp✝ }).support = { toFinsupp := toFinsupp✝ }.support

Proof state:
case ofFinsupp
R : Type u
inst✝ : Ring R
toFinsupp✝ : R[ℕ]
⊢ (-{ toFinsupp := toFinsupp✝ }).support = { toFinsupp := toFinsupp✝ }.support

Tactic:
rw [← ofFinsupp_neg, support, support, Finsupp.support_neg]

Result:
no goals
-- Mathlib/Topology/Sets/Closeds.lean
theorem Opens.isCoatom_iff [T1Space α] {s : Opens α} :
    IsCoatom s ↔ ∃ x, s = (Closeds.singleton x).compl

Proof state:
α : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s : Opens α
⊢ IsCoatom s ↔ ∃ x, s = (Closeds.singleton x).compl

Tactic:
rw [← s.compl_compl, ← isAtom_dual_iff_isCoatom]

Result:
α : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s : Opens α
⊢ IsAtom (toDual s.compl.compl) ↔ ∃ x, s.compl.compl = (Closeds.singleton x).compl

Proof state:
α : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s : Opens α
⊢ IsAtom ((Closeds.complOrderIso α) s.compl) ↔ ∃ x, s.compl.compl = (Closeds.singleton x).compl

Tactic:
simp only [(Closeds.complOrderIso α).isAtom_iff, Closeds.isAtom_iff,
  Closeds.compl_bijective.injective.eq_iff]

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s : Opens α
⊢ IsAtom (toDual s.compl.compl) ↔ ∃ x, s.compl.compl = (Closeds.singleton x).compl

Tactic:
change IsAtom (Closeds.complOrderIso α s.compl) ↔ _

Result:
α : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s : Opens α
⊢ IsAtom ((Closeds.complOrderIso α) s.compl) ↔ ∃ x, s.compl.compl = (Closeds.singleton x).compl
-- Mathlib/Order/Irreducible.lean
theorem SupIrred.finset_sup_eq (ha : SupIrred a) (h : s.sup f = a) : ∃ i ∈ s, f i = a

Proof state:
case empty
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
a : α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
ha : SupIrred a
h : ∅.sup f = a
⊢ ∃ i ∈ ∅, f i = a

Tactic:
simpa [ha.ne_bot] using h.symm

Result:
no goals

Proof state:
case insert
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
a : α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
ha : SupIrred a
i : ι
s : Finset ι
a✝ : i ∉ s
ih : s.sup f = a → ∃ i ∈ s, f i = a
h : f i ⊔ s.sup f = a
⊢ f i = a ∨ ∃ x ∈ s, f x = a

Tactic:
exact (ha.2 h).imp_right ih

Result:
no goals

Proof state:
case insert
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
a : α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
ha : SupIrred a
i : ι
s : Finset ι
a✝ : i ∉ s
ih : s.sup f = a → ∃ i ∈ s, f i = a
h : (insert i s).sup f = a
⊢ f i = a ∨ ∃ x ∈ s, f x = a

Tactic:
rw [sup_insert] at h

Result:
case insert
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
a : α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
ha : SupIrred a
i : ι
s : Finset ι
a✝ : i ∉ s
ih : s.sup f = a → ∃ i ∈ s, f i = a
h : f i ⊔ s.sup f = a
⊢ f i = a ∨ ∃ x ∈ s, f x = a

Proof state:
case insert
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
a : α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
ha : SupIrred a
i : ι
s : Finset ι
a✝ : i ∉ s
ih : s.sup f = a → ∃ i ∈ s, f i = a
h : (insert i s).sup f = a
⊢ ∃ i_1 ∈ insert i s, f i_1 = a

Tactic:
simp only [exists_prop, exists_mem_insert] at ih ⊢

Result:
case insert
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
a : α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
ha : SupIrred a
i : ι
s : Finset ι
a✝ : i ∉ s
ih : s.sup f = a → ∃ i ∈ s, f i = a
h : (insert i s).sup f = a
⊢ f i = a ∨ ∃ x ∈ s, f x = a

Proof state:
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
a : α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
ha : SupIrred a
h : s.sup f = a
⊢ ∃ i ∈ s, f i = a

Tactic:
induction' s using Finset.induction with i s _ ih

Result:
case empty
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
a : α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
ha : SupIrred a
h : ∅.sup f = a
⊢ ∃ i ∈ ∅, f i = a

case insert
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
a : α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
ha : SupIrred a
i : ι
s : Finset ι
a✝ : i ∉ s
ih : s.sup f = a → ∃ i ∈ s, f i = a
h : (insert i s).sup f = a
⊢ ∃ i_1 ∈ insert i s, f i_1 = a
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem self_eq_add_left {x y : BitVec w} : x = y + x ↔ y = 0#w

Proof state:
w : Nat
x y : BitVec w
⊢ x = y + x ↔ y = 0#w

Tactic:
rw [BitVec.add_comm]

Result:
w : Nat
x y : BitVec w
⊢ x = x + y ↔ y = 0#w

Proof state:
w : Nat
x y : BitVec w
⊢ x = x + y ↔ y = 0#w

Tactic:
exact BitVec.self_eq_add_right

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma Y_ne_negY_of_Y_ne' [NoZeroDivisors R] {P Q : Fin 3 → R} (hP : W'.Equation P)
    (hQ : W'.Equation Q) (hPz : P z ≠ 0) (hQz : Q z ≠ 0) (hx : P x * Q z = Q x * P z)
    (hy : P y * Q z ≠ W'.negY Q * P z) : P y ≠ W'.negY P

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z ≠ W'.negY Q * P z
hy' : P y * Q z - Q y * P z = 0
⊢ P y ≠ W'.negY P

Tactic:
contrapose! hy

Result:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy' : P y * Q z - Q y * P z = 0
hy : P y = W'.negY P
⊢ P y * Q z = W'.negY Q * P z

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z ≠ W'.negY Q * P z
⊢ P y ≠ W'.negY P

Tactic:
have hy' : P y * Q z - Q y * P z = 0 := sub_eq_zero.mpr <| Y_eq_of_Y_ne' hP hQ hPz hQz hx hy

Result:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z ≠ W'.negY Q * P z
hy' : P y * Q z - Q y * P z = 0
⊢ P y ≠ W'.negY P

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy' : P y * Q z - Q y * P z = 0
hy : P y = W'.negY P
⊢ P y * Q z = W'.negY Q * P z

Tactic:
linear_combination (norm := ring1) Y_sub_Y_add_Y_sub_negY hx + Q z * hy - hy'

Result:
no goals
-- Mathlib/Topology/Homotopy/HSpaces.lean
theorem continuous_qRight : Continuous qRight :=
  continuous_projIcc.comp <|
    Continuous.div (by fun_prop) (by fun_prop) fun _ ↦ (add_pos zero_lt_one).ne'

Proof state:
⊢ Continuous fun p => 1 + ↑p.2

Tactic:
fun_prop

Result:
no goals

Proof state:
⊢ Continuous fun p => 2 * ↑p.1

Tactic:
fun_prop

Result:
no goals
-- Mathlib/Topology/Bases.lean
theorem Topology.IsInducing.secondCountableTopology [TopologicalSpace β]
    [SecondCountableTopology β] (hf : IsInducing f) : SecondCountableTopology α

Proof state:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : SecondCountableTopology β
hf : IsInducing f
⊢ SecondCountableTopology α

Tactic:
exact secondCountableTopology_induced α β f

Result:
no goals
-- Mathlib/LinearAlgebra/TensorPower/Basic.lean
theorem mul_algebraMap₀ {n} (r : R) (a : ⨂[R]^n M) :
    cast R M (add_zero _) (a ₜ* algebraMap₀ r) = r • a

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
r : R
a : ⨂[R]^n M
⊢ (cast R M ⋯) (GradedMonoid.GMul.mul a (algebraMap₀ r)) = r • a

Tactic:
rw [gMul_eq_coe_linearMap, algebraMap₀_eq_smul_one, LinearMap.map_smul,
  LinearEquiv.map_smul, ← gMul_eq_coe_linearMap, mul_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Norm.lean
theorem imp_self_eq (p : Prop) : (p → p) = True

Proof state:
p : Prop
⊢ (p → p) = True

Tactic:
simp

Result:
no goals