harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/QuadraticDiscriminant.lean
theorem quadratic_eq_zero_iff_discrim_eq_sq [NeZero (2 : R)] [NoZeroDivisors R]
    (ha : a ≠ 0) (x : R) :
    a * (x * x) + b * x + c = 0 ↔ discrim a b c = (2 * a * x + b) ^ 2

Proof state:
R : Type u_1
inst✝² : CommRing R
a b c : R
inst✝¹ : NeZero 2
inst✝ : NoZeroDivisors R
ha : a ≠ 0
x : R
⊢ a * (x * x) + b * x + c = 0 ↔ discrim a b c = (2 * a * x + b) ^ 2

Tactic:
refine ⟨discrim_eq_sq_of_quadratic_eq_zero, fun h ↦ ?_⟩

Result:
R : Type u_1
inst✝² : CommRing R
a b c : R
inst✝¹ : NeZero 2
inst✝ : NoZeroDivisors R
ha : a ≠ 0
x : R
h : discrim a b c = (2 * a * x + b) ^ 2
⊢ a * (x * x) + b * x + c = 0

Proof state:
R : Type u_1
inst✝² : CommRing R
a b c : R
inst✝¹ : NeZero 2
inst✝ : NoZeroDivisors R
ha : a ≠ 0
x : R
h : discrim a b c = (2 * a * x + b) ^ 2
⊢ a * (x * x) + b * x + c = 0

Tactic:
rw [discrim] at h

Result:
R : Type u_1
inst✝² : CommRing R
a b c : R
inst✝¹ : NeZero 2
inst✝ : NoZeroDivisors R
ha : a ≠ 0
x : R
h : b ^ 2 - 4 * a * c = (2 * a * x + b) ^ 2
⊢ a * (x * x) + b * x + c = 0

Proof state:
R : Type u_1
inst✝² : CommRing R
a b c : R
inst✝¹ : NeZero 2
inst✝ : NoZeroDivisors R
ha : a ≠ 0
x : R
h : b ^ 2 - 4 * a * c = (2 * a * x + b) ^ 2
⊢ a * (x * x) + b * x + c = 0

Tactic:
have ha : 2 * 2 * a ≠ 0 := mul_ne_zero (mul_ne_zero (NeZero.ne _) (NeZero.ne _)) ha

Result:
R : Type u_1
inst✝² : CommRing R
a b c : R
inst✝¹ : NeZero 2
inst✝ : NoZeroDivisors R
ha✝ : a ≠ 0
x : R
h : b ^ 2 - 4 * a * c = (2 * a * x + b) ^ 2
ha : 2 * 2 * a ≠ 0
⊢ a * (x * x) + b * x + c = 0

Proof state:
R : Type u_1
inst✝² : CommRing R
a b c : R
inst✝¹ : NeZero 2
inst✝ : NoZeroDivisors R
ha✝ : a ≠ 0
x : R
h : b ^ 2 - 4 * a * c = (2 * a * x + b) ^ 2
ha : 2 * 2 * a ≠ 0
⊢ a * (x * x) + b * x + c = 0

Tactic:
apply mul_left_cancel₀ ha

Result:
R : Type u_1
inst✝² : CommRing R
a b c : R
inst✝¹ : NeZero 2
inst✝ : NoZeroDivisors R
ha✝ : a ≠ 0
x : R
h : b ^ 2 - 4 * a * c = (2 * a * x + b) ^ 2
ha : 2 * 2 * a ≠ 0
⊢ 2 * 2 * a * (a * (x * x) + b * x + c) = 2 * 2 * a * 0

Proof state:
R : Type u_1
inst✝² : CommRing R
a b c : R
inst✝¹ : NeZero 2
inst✝ : NoZeroDivisors R
ha✝ : a ≠ 0
x : R
h : b ^ 2 - 4 * a * c = (2 * a * x + b) ^ 2
ha : 2 * 2 * a ≠ 0
⊢ 2 * 2 * a * (a * (x * x) + b * x + c) = 2 * 2 * a * 0

Tactic:
linear_combination -h

Result:
no goals
-- Mathlib/RingTheory/FinitePresentation.lean
/-- Induction principle for finitely presented ring homomorphisms.

For a property to hold for all finitely presented ring homs, it suffices for it to hold for
`Polynomial.C : R → R[X]`, surjective ring homs with finitely generated kernels, and to be closed
under composition.

Note that to state this conveniently for ring homs between rings of different universes, we carry
around two predicates `P` and `Q`, which should be "the same" apart from universes:
* `P`, for ring homs `(R : Type u) → (S : Type u)`.
* `Q`, for ring homs `(R : Type u) → (S : Type v)`.
-/
lemma polynomial_induction
    (P : ∀ (R : Type u) [CommRing R] (S : Type u) [CommRing S], (R →+* S) → Prop)
    (Q : ∀ (R : Type u) [CommRing R] (S : Type v) [CommRing S], (R →+* S) → Prop)
    (polynomial : ∀ (R) [CommRing R], P R R[X] C)
    (fg_ker : ∀ (R : Type u) [CommRing R] (S : Type v) [CommRing S] (f : R →+* S),
      Surjective f → (ker f).FG → Q R S f)
    (comp : ∀ (R) [CommRing R] (S) [CommRing S] (T) [CommRing T] (f : R →+* S) (g : S →+* T),
      P R S f → Q S T g → Q R T (g.comp f))
    {R : Type u} {S : Type v} [CommRing R] [CommRing S] (f : R →+* S) (hf : f.FinitePresentation) :
    Q R S f

Proof state:
case h.e'_3
P : (R : Type u) → [inst : CommRing R] → (S : Type u) → [inst_1 : CommRing S] → (R →+* S) → Prop
Q : (R : Type u) → [inst : CommRing R] → (S : Type v) → [inst_1 : CommRing S] → (R →+* S) → Prop
polynomial : ∀ (R : Type u) [inst : CommRing R], P R R[X] C
fg_ker :
  ∀ (R : Type u) [inst : CommRing R] (S : Type v) [inst_1 : CommRing S] (f : R →+* S),
    Surjective ⇑f → (ker f).FG → Q R S f
comp :
  ∀ (R : Type u) [inst : CommRing R] (S : Type u) [inst_1 : CommRing S] (T : Type v) [inst_2 : CommRing T] (f : R →+* S)
    (g : S →+* T), P R S f → Q S T g → Q R T (g.comp f)
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
g' : MvPolynomial (Fin 0) R →+* S
hg : Surjective ⇑g'
hg' : (ker g').FG
this : Algebra R S := (g'.comp MvPolynomial.C).toAlgebra
⊢ Ideal.comap MvPolynomial.C (ker g') = Ideal.map (MvPolynomial.isEmptyRingEquiv R (Fin 0)).toRingHom (ker g')

Tactic:
simp only [RingEquiv.toRingHom_eq_coe]

Result:
case h.e'_3
P : (R : Type u) → [inst : CommRing R] → (S : Type u) → [inst_1 : CommRing S] → (R →+* S) → Prop
Q : (R : Type u) → [inst : CommRing R] → (S : Type v) → [inst_1 : CommRing S] → (R →+* S) → Prop
polynomial : ∀ (R : Type u) [inst : CommRing R], P R R[X] C
fg_ker :
  ∀ (R : Type u) [inst : CommRing R] (S : Type v) [inst_1 : CommRing S] (f : R →+* S),
    Surjective ⇑f → (ker f).FG → Q R S f
comp :
  ∀ (R : Type u) [inst : CommRing R] (S : Type u) [inst_1 : CommRing S] (T : Type v) [inst_2 : CommRing T] (f : R →+* S)
    (g : S →+* T), P R S f → Q S T g → Q R T (g.comp f)
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
g' : MvPolynomial (Fin 0) R →+* S
hg : Surjective ⇑g'
hg' : (ker g').FG
this : Algebra R S := (g'.comp MvPolynomial.C).toAlgebra
⊢ Ideal.comap MvPolynomial.C (ker g') = Ideal.map (↑(MvPolynomial.isEmptyRingEquiv R (Fin 0))) (ker g')
-- Mathlib/Data/Nat/Totient.lean
theorem totient_pos {n : ℕ} : 0 < φ n ↔ 0 < n

Proof state:
n : ℕ
⊢ 0 < φ n ↔ 0 < n

Tactic:
simp [pos_iff_ne_zero]

Result:
no goals
-- Mathlib/GroupTheory/DoubleCoset.lean
theorem rel_bot_eq_right_group_rel (H : Subgroup G) :
    ⇑(setoid ↑H ↑(⊥ : Subgroup G)) = ⇑(QuotientGroup.rightRel H)

Proof state:
case h.h.a.mp
G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
⊢ (∃ a_1 ∈ H, ∃ b_1 ∈ ⊥, b = a_1 * a * b_1) → b * a⁻¹ ∈ H

Tactic:
rintro ⟨b, hb, a, rfl : a = 1, rfl⟩

Result:
case h.h.a.mp.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
hb : b ∈ H
⊢ b * a * 1 * a⁻¹ ∈ H

Proof state:
case h.h.a.mpr
G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
h : b * a⁻¹ ∈ H
⊢ ∃ a_1 ∈ H, ∃ b_1 ∈ ⊥, b = a_1 * a * b_1

Tactic:
exact ⟨b * a⁻¹, h, 1, rfl, by rw [mul_one, inv_mul_cancel_right]⟩

Result:
no goals

Proof state:
case h.h.a.mpr
G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
⊢ b * a⁻¹ ∈ H → ∃ a_2 ∈ H, ∃ b_1 ∈ ⊥, b = a_2 * a * b_1

Tactic:
rintro (h : b * a⁻¹ ∈ H)

Result:
case h.h.a.mpr
G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
h : b * a⁻¹ ∈ H
⊢ ∃ a_1 ∈ H, ∃ b_1 ∈ ⊥, b = a_1 * a * b_1

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
h : b * a⁻¹ ∈ H
⊢ b = b * a⁻¹ * a * 1

Tactic:
rw [mul_one, inv_mul_cancel_right]

Result:
no goals

Proof state:
case h.h.a
G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
⊢ (setoid ↑H ↑⊥) a b ↔ (QuotientGroup.rightRel H) a b

Tactic:
rw [rel_iff, QuotientGroup.rightRel_apply]

Result:
case h.h.a
G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
⊢ (∃ a_1 ∈ H, ∃ b_1 ∈ ⊥, b = a_1 * a * b_1) ↔ b * a⁻¹ ∈ H

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ⇑(setoid ↑H ↑⊥) = ⇑(QuotientGroup.rightRel H)

Tactic:
ext a b

Result:
case h.h.a
G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
⊢ (setoid ↑H ↑⊥) a b ↔ (QuotientGroup.rightRel H) a b

Proof state:
case h.h.a
G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
⊢ (∃ a_1 ∈ H, ∃ b_1 ∈ ⊥, b = a_1 * a * b_1) ↔ b * a⁻¹ ∈ H

Tactic:
constructor

Result:
case h.h.a.mp
G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
⊢ (∃ a_1 ∈ H, ∃ b_1 ∈ ⊥, b = a_1 * a * b_1) → b * a⁻¹ ∈ H

case h.h.a.mpr
G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
⊢ b * a⁻¹ ∈ H → ∃ a_2 ∈ H, ∃ b_1 ∈ ⊥, b = a_2 * a * b_1

Proof state:
case h.h.a.mp.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
hb : b ∈ H
⊢ b * a * 1 * a⁻¹ ∈ H

Tactic:
rwa [mul_one, mul_inv_cancel_right]

Result:
no goals
-- Mathlib/Order/Part.lean
lemma Monotone.partBind (hf : Monotone f) (hg : Monotone g) :
    Monotone fun x ↦ (f x).bind (g x)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Preorder α
f : α → Part β
g : α → β → Part γ
hf : Monotone f
hg : Monotone g
⊢ Monotone fun x => (f x).bind (g x)

Tactic:
rintro x y h a

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Preorder α
f : α → Part β
g : α → β → Part γ
hf : Monotone f
hg : Monotone g
x y : α
h : x ≤ y
a : γ
⊢ a ∈ (fun x => (f x).bind (g x)) x → a ∈ (fun x => (f x).bind (g x)) y

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Preorder α
f : α → Part β
g : α → β → Part γ
hf : Monotone f
hg : Monotone g
x y : α
h : x ≤ y
a : γ
⊢ ∀ x_1 ∈ f x, a ∈ g x x_1 → ∃ a_3 ∈ f y, a ∈ g y a_3

Tactic:
exact fun b hb ha ↦ ⟨b, hf h _ hb, hg h _ _ ha⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Preorder α
f : α → Part β
g : α → β → Part γ
hf : Monotone f
hg : Monotone g
x y : α
h : x ≤ y
a : γ
⊢ a ∈ (fun x => (f x).bind (g x)) x → a ∈ (fun x => (f x).bind (g x)) y

Tactic:
simp only [and_imp, exists_prop, Part.bind_eq_bind, Part.mem_bind_iff, exists_imp]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Preorder α
f : α → Part β
g : α → β → Part γ
hf : Monotone f
hg : Monotone g
x y : α
h : x ≤ y
a : γ
⊢ ∀ x_1 ∈ f x, a ∈ g x x_1 → ∃ a_3 ∈ f y, a ∈ g y a_3
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
lemma coeSubgraph_le {H : G.Subgraph} (H' : H.coe.Subgraph) :
    Subgraph.coeSubgraph H' ≤ H

Proof state:
V : Type u
G : SimpleGraph V
H : G.Subgraph
H' : H.coe.Subgraph
⊢ Subgraph.coeSubgraph H' ≤ H

Tactic:
constructor

Result:
case left
V : Type u
G : SimpleGraph V
H : G.Subgraph
H' : H.coe.Subgraph
⊢ (Subgraph.coeSubgraph H').verts ⊆ H.verts

case right
V : Type u
G : SimpleGraph V
H : G.Subgraph
H' : H.coe.Subgraph
⊢ ∀ ⦃v w : V⦄, (Subgraph.coeSubgraph H').Adj v w → H.Adj v w

Proof state:
case right
V : Type u
G : SimpleGraph V
H : G.Subgraph
H' : H.coe.Subgraph
⊢ ∀ ⦃v w : V⦄, (Subgraph.coeSubgraph H').Adj v w → H.Adj v w

Tactic:
rintro v w ⟨_, _, h, rfl, rfl⟩

Result:
case right.intro.intro.intro.intro
V : Type u
G : SimpleGraph V
H : G.Subgraph
H' : H.coe.Subgraph
w✝¹ w✝ : ↑H.verts
h : H'.Adj w✝¹ w✝
⊢ H.Adj (H.hom w✝¹) (H.hom w✝)

Proof state:
case left
V : Type u
G : SimpleGraph V
H : G.Subgraph
H' : H.coe.Subgraph
⊢ (Subgraph.coeSubgraph H').verts ⊆ H.verts

Tactic:
simp

Result:
no goals

Proof state:
case right.intro.intro.intro.intro
V : Type u
G : SimpleGraph V
H : G.Subgraph
H' : H.coe.Subgraph
w✝¹ w✝ : ↑H.verts
h : H'.Adj w✝¹ w✝
⊢ H.Adj (H.hom w✝¹) (H.hom w✝)

Tactic:
exact H'.adj_sub h

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
lemma eLpNormEssSup_indicator_le (s : Set α) (f : α → G) :
    eLpNormEssSup (s.indicator f) μ ≤ eLpNormEssSup f μ

Proof state:
α : Type u_1
G : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
s : Set α
f : α → G
x : α
⊢ s.indicator (fun a => ‖f a‖₊) x ≤ ‖f x‖₊

Tactic:
exact Set.indicator_le_self s _ x

Result:
no goals

Proof state:
α : Type u_1
G : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
s : Set α
f : α → G
x : α
⊢ (fun x => ‖s.indicator f x‖ₑ) x ≤ (fun x => ‖f x‖ₑ) x

Tactic:
simp_rw [enorm_eq_nnnorm, ENNReal.coe_le_coe, nnnorm_indicator_eq_indicator_nnnorm]

Result:
α : Type u_1
G : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
s : Set α
f : α → G
x : α
⊢ s.indicator (fun a => ‖f a‖₊) x ≤ ‖f x‖₊

Proof state:
α : Type u_1
G : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
s : Set α
f : α → G
⊢ eLpNormEssSup (s.indicator f) μ ≤ eLpNormEssSup f μ

Tactic:
refine essSup_mono_ae (Eventually.of_forall fun x => ?_)

Result:
α : Type u_1
G : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
s : Set α
f : α → G
x : α
⊢ (fun x => ‖s.indicator f x‖ₑ) x ≤ (fun x => ‖f x‖ₑ) x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem takeWhile_map (f : α → β) (p : β → Bool) (l : List α) :
    (l.map f).takeWhile p = (l.takeWhile (p ∘ f)).map f

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → β
p : β → Bool
x : α
xs : List α
ih : takeWhile p (map f xs) = map f (takeWhile (p ∘ f) xs)
⊢ (if p (f x) = true then f x :: takeWhile p (map f xs) else []) =
    map f (if (p ∘ f) x = true then x :: takeWhile (p ∘ f) xs else [])

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → β
p : β → Bool
x : α
xs : List α
ih : takeWhile p (map f xs) = map f (takeWhile (p ∘ f) xs)
⊢ takeWhile p (map f (x :: xs)) = map f (takeWhile (p ∘ f) (x :: xs))

Tactic:
simp only [map_cons, takeWhile_cons]

Result:
case cons
α : Type u_1
β : Type u_2
f : α → β
p : β → Bool
x : α
xs : List α
ih : takeWhile p (map f xs) = map f (takeWhile (p ∘ f) xs)
⊢ (if p (f x) = true then f x :: takeWhile p (map f xs) else []) =
    map f (if (p ∘ f) x = true then x :: takeWhile (p ∘ f) xs else [])

Proof state:
α : Type u_1
β : Type u_2
f : α → β
p : β → Bool
l : List α
⊢ takeWhile p (map f l) = map f (takeWhile (p ∘ f) l)

Tactic:
induction l with
| nil => rfl
| cons x xs ih =>
  simp only [map_cons, takeWhile_cons]
  split <;> simp_all

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
f : α → β
p : β → Bool
⊢ takeWhile p (map f []) = map f (takeWhile (p ∘ f) [])

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Dialectica/Monoidal.lean
theorem leftUnitor_naturality {X Y : Dial C} (f : X ⟶ Y) :
    (𝟙 (𝟙_ (Dial C)) ⊗ f) ≫ (λ_ Y).hom = (λ_ X).hom ≫ f

Proof state:
case hF.h₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
f : X ⟶ Y
⊢ π(terminal.from (((⊤_ C) ⨯ X.src) ⨯ Y.tgt), π(π₁ ≫ π₂, π₂) ≫ f.F) ≫ π₂ =
    π(terminal.from (((⊤_ C) ⨯ X.src) ⨯ Y.tgt), prod.map π₂ (𝟙 Y.tgt) ≫ f.F) ≫ π₂

Tactic:
simp

Result:
case hF.h₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
f : X ⟶ Y
⊢ π(π₁ ≫ π₂, π₂) ≫ f.F = prod.map π₂ (𝟙 Y.tgt) ≫ f.F

Proof state:
case hF.h₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
f : X ⟶ Y
⊢ π(π₁ ≫ π₂, π₂) ≫ f.F = prod.map π₂ (𝟙 Y.tgt) ≫ f.F

Tactic:
congr 1

Result:
case hF.h₂.e_a
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
f : X ⟶ Y
⊢ π(π₁ ≫ π₂, π₂) = prod.map π₂ (𝟙 Y.tgt)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
f : X ⟶ Y
⊢ (𝟙 (𝟙_ (Dial C)) ⊗ f) ≫ (λ_ Y).hom = (λ_ X).hom ≫ f

Tactic:
ext <;> simp

Result:
case hF
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
f : X ⟶ Y
⊢ π(terminal.from (((⊤_ C) ⨯ X.src) ⨯ Y.tgt), π(π₁ ≫ π₂, π₂) ≫ f.F) =
    π(terminal.from (((⊤_ C) ⨯ X.src) ⨯ Y.tgt), prod.map π₂ (𝟙 Y.tgt) ≫ f.F)

Proof state:
case hF
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
f : X ⟶ Y
⊢ π(terminal.from (((⊤_ C) ⨯ X.src) ⨯ Y.tgt), π(π₁ ≫ π₂, π₂) ≫ f.F) =
    π(terminal.from (((⊤_ C) ⨯ X.src) ⨯ Y.tgt), prod.map π₂ (𝟙 Y.tgt) ≫ f.F)

Tactic:
ext

Result:
case hF.h₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
f : X ⟶ Y
⊢ π(terminal.from (((⊤_ C) ⨯ X.src) ⨯ Y.tgt), π(π₁ ≫ π₂, π₂) ≫ f.F) ≫ π₂ =
    π(terminal.from (((⊤_ C) ⨯ X.src) ⨯ Y.tgt), prod.map π₂ (𝟙 Y.tgt) ≫ f.F) ≫ π₂

Proof state:
case hF.h₂.e_a
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
f : X ⟶ Y
⊢ π(π₁ ≫ π₂, π₂) = prod.map π₂ (𝟙 Y.tgt)

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Algebra/Order/Group/Lattice.lean
@[to_additive]
lemma pow_two_semiclosed
    {a : α} (ha : 1 ≤ a ^ 2) : 1 ≤ a

Proof state:
α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
ha : 1 ≤ a ^ 2
⊢ (a ⊓ 1) * (a ⊓ 1) = a ⊓ 1

Tactic:
rw [mul_inf, inf_mul, ← pow_two, mul_one, one_mul, inf_assoc, inf_left_idem, inf_comm,
  inf_assoc, inf_of_le_left ha]

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
ha : 1 ≤ a ^ 2
this : (a ⊓ 1) * (a ⊓ 1) = a ⊓ 1
⊢ 1 ≤ a

Tactic:
rwa [← inf_eq_right, ← mul_right_eq_self]

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
ha : 1 ≤ a ^ 2
⊢ 1 ≤ a

Tactic:
suffices this : (a ⊓ 1) * (a ⊓ 1) = a ⊓ 1 by
  rwa [← inf_eq_right, ← mul_right_eq_self]

Result:
α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
ha : 1 ≤ a ^ 2
⊢ (a ⊓ 1) * (a ⊓ 1) = a ⊓ 1
-- Mathlib/MeasureTheory/Measure/Hausdorff.lean
theorem trim_mkMetric [MeasurableSpace X] [BorelSpace X] (m : ℝ≥0∞ → ℝ≥0∞) :
    (mkMetric m : OuterMeasure X).trim = mkMetric m

Proof state:
case e_s.h
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
n : ℕ
⊢ (mkMetric'.pre (fun s => m (diam s)) (↑n)⁻¹).trim = mkMetric'.pre (fun s => m (diam s)) (↑n)⁻¹

Tactic:
refine mkMetric'.trim_pre _ (fun s => ?_) _

Result:
case e_s.h
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
n : ℕ
s : Set X
⊢ m (diam (closure s)) = m (diam s)

Proof state:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
⊢ ⨆ i, (mkMetric'.pre (fun s => m (diam s)) (↑i)⁻¹).trim = ⨆ n, mkMetric'.pre (fun s => m (diam s)) (↑n)⁻¹

Tactic:
congr 1 with n : 1

Result:
case e_s.h
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
n : ℕ
⊢ (mkMetric'.pre (fun s => m (diam s)) (↑n)⁻¹).trim = mkMetric'.pre (fun s => m (diam s)) (↑n)⁻¹

Proof state:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
⊢ (mkMetric m).trim = mkMetric m

Tactic:
simp only [mkMetric, mkMetric'.eq_iSup_nat, trim_iSup]

Result:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
⊢ ⨆ i, (mkMetric'.pre (fun s => m (diam s)) (↑i)⁻¹).trim = ⨆ n, mkMetric'.pre (fun s => m (diam s)) (↑n)⁻¹

Proof state:
case e_s.h
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
n : ℕ
s : Set X
⊢ m (diam (closure s)) = m (diam s)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem mem_attach (l : Vector α n) : ∀ x, x ∈ l.attach
  | ⟨a, h⟩ => by
    have := mem_map.1 (by rw [attach_map_subtype_val] <;> exact h)
    rcases this with ⟨⟨_, _⟩, m, rfl⟩
    exact m

Proof state:
α : Type u_1
n : Nat
l : Vector α n
a : α
h : a ∈ l
⊢ ?m.24974 ∈ map ?m.24975 ?m.24976

Tactic:
rw [attach_map_subtype_val] <;> exact h

Result:
no goals

Proof state:
case intro.mk.intro
α : Type u_1
n : Nat
l : Vector α n
val✝ : α
property✝ : val✝ ∈ l
m : ⟨val✝, property✝⟩ ∈ l.attach
h : ⟨val✝, property✝⟩.val ∈ l
⊢ ⟨⟨val✝, property✝⟩.val, h⟩ ∈ l.attach

Tactic:
exact m

Result:
no goals

Proof state:
α : Type u_1
n : Nat
l : Vector α n
a : α
h : a ∈ l
this : ∃ a_1, a_1 ∈ l.attach ∧ a_1.val = a
⊢ ⟨a, h⟩ ∈ l.attach

Tactic:
rcases this with ⟨⟨_, _⟩, m, rfl⟩

Result:
case intro.mk.intro
α : Type u_1
n : Nat
l : Vector α n
val✝ : α
property✝ : val✝ ∈ l
m : ⟨val✝, property✝⟩ ∈ l.attach
h : ⟨val✝, property✝⟩.val ∈ l
⊢ ⟨⟨val✝, property✝⟩.val, h⟩ ∈ l.attach

Proof state:
α : Type u_1
n : Nat
l : Vector α n
a : α
h : a ∈ l
⊢ ⟨a, h⟩ ∈ l.attach

Tactic:
have := mem_map.1 (by rw [attach_map_subtype_val] <;> exact h)

Result:
α : Type u_1
n : Nat
l : Vector α n
a : α
h : a ∈ l
this : ∃ a_1, a_1 ∈ l.attach ∧ a_1.val = a
⊢ ⟨a, h⟩ ∈ l.attach
-- Mathlib/Probability/Kernel/WithDensity.lean
theorem isSFiniteKernel_withDensity_of_isFiniteKernel (κ : Kernel α β) [IsFiniteKernel κ]
    (hf_ne_top : ∀ a b, f a b ≠ ∞) : IsSFiniteKernel (withDensity κ f)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ⊤
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ := fun n a b => f a b ⊓ (↑n + 1) - f a b ⊓ ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ ↑n
a : α
b : β
n : ℕ
hn : ⌈(f a b).toReal⌉₊ ≤ n
⊢ fs n a b = 0

Tactic:
suffices min (f a b) (n + 1) = f a b ∧ min (f a b) n = f a b by
  simp_rw [fs, this.1, this.2, tsub_self (f a b)]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ⊤
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ := fun n a b => f a b ⊓ (↑n + 1) - f a b ⊓ ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ ↑n
a : α
b : β
n : ℕ
hn : ⌈(f a b).toReal⌉₊ ≤ n
⊢ f a b ⊓ (↑n + 1) = f a b ∧ f a b ⊓ ↑n = f a b

Proof state:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ⊤
hf : ¬Measurable (Function.uncurry f)
⊢ IsSFiniteKernel (κ.withDensity f)

Tactic:
rw [withDensity_of_not_measurable _ hf]

Result:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ⊤
hf : ¬Measurable (Function.uncurry f)
⊢ IsSFiniteKernel 0
-- Mathlib/Algebra/Homology/ShortComplex/ModuleCat.lean
lemma ShortExact.moduleCat_exact_iff_function_exact :
    S.Exact ↔ Function.Exact S.f S.g

Proof state:
R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
⊢ LinearMap.range (ModuleCat.Hom.hom S.f) = LinearMap.ker (ModuleCat.Hom.hom S.g) ↔
    LinearMap.ker (ConcreteCategory.hom S.g) = LinearMap.range (ConcreteCategory.hom S.f)

Tactic:
tauto

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
⊢ S.Exact ↔ Function.Exact ⇑(ConcreteCategory.hom S.f) ⇑(ConcreteCategory.hom S.g)

Tactic:
rw [moduleCat_exact_iff_range_eq_ker, LinearMap.exact_iff]

Result:
R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
⊢ LinearMap.range (ModuleCat.Hom.hom S.f) = LinearMap.ker (ModuleCat.Hom.hom S.g) ↔
    LinearMap.ker (ConcreteCategory.hom S.g) = LinearMap.range (ConcreteCategory.hom S.f)
-- Mathlib/LinearAlgebra/Matrix/Ideal.lean
theorem matricesOver_top : (⊤ : TwoSidedIdeal R).matricesOver n = ⊤

Proof state:
R : Type u_1
inst✝¹ : Ring R
n : Type u_2
inst✝ : Fintype n
⊢ matricesOver n ⊤ = ⊤

Tactic:
ext

Result:
case h
R : Type u_1
inst✝¹ : Ring R
n : Type u_2
inst✝ : Fintype n
x✝ : Matrix n n R
⊢ x✝ ∈ matricesOver n ⊤ ↔ x✝ ∈ ⊤

Proof state:
case h
R : Type u_1
inst✝¹ : Ring R
n : Type u_2
inst✝ : Fintype n
x✝ : Matrix n n R
⊢ x✝ ∈ matricesOver n ⊤ ↔ x✝ ∈ ⊤

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Symmetric/NewtonIdentities.lean
theorem disjoint_filter_pairs_lt_filter_pairs_eq (k : ℕ) :
    Disjoint {t ∈ pairs σ k | #t.1 < k} {t ∈ pairs σ k | #t.1 = k}

Proof state:
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
⊢ Disjoint (filter (fun t => #t.1 < k) (MvPolynomial.NewtonIdentities.pairs σ k))
    (filter (fun t => #t.1 = k) (MvPolynomial.NewtonIdentities.pairs σ k))

Tactic:
rw [disjoint_filter]

Result:
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
⊢ ∀ x ∈ MvPolynomial.NewtonIdentities.pairs σ k, #x.1 < k → ¬#x.1 = k

Proof state:
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
⊢ ∀ x ∈ MvPolynomial.NewtonIdentities.pairs σ k, #x.1 < k → ¬#x.1 = k

Tactic:
exact fun _ _ h1 h2 ↦ lt_irrefl _ (h2.symm.subst h1)

Result:
no goals