harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/CompleteLattice/Finset.lean
theorem iSup_insert (a : α) (s : Finset α) (t : α → β) :
    ⨆ x ∈ insert a s, t x = t a ⊔ ⨆ x ∈ s, t x

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CompleteLattice β
inst✝ : DecidableEq α
a : α
s : Finset α
t : α → β
⊢ ⨆ x ∈ insert a s, t x = t a ⊔ ⨆ x ∈ s, t x

Tactic:
rw [insert_eq]

Result:
α : Type u_2
β : Type u_3
inst✝¹ : CompleteLattice β
inst✝ : DecidableEq α
a : α
s : Finset α
t : α → β
⊢ ⨆ x ∈ {a} ∪ s, t x = t a ⊔ ⨆ x ∈ s, t x

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CompleteLattice β
inst✝ : DecidableEq α
a : α
s : Finset α
t : α → β
⊢ ⨆ x ∈ {a} ∪ s, t x = t a ⊔ ⨆ x ∈ s, t x

Tactic:
simp only [iSup_union, Finset.iSup_singleton]

Result:
no goals
-- Mathlib/Algebra/Quaternion.lean
@[norm_cast, simp]
lemma coe_ofNat {n : ℕ} [n.AtLeastTwo]:
    ((ofNat(n) : R) : ℍ[R,c₁,c₂,c₃]) = (ofNat(n) : ℍ[R,c₁,c₂,c₃])

Proof state:
R : Type u_3
c₁ c₂ c₃ : R
inst✝¹ : CommRing R
n : ℕ
inst✝ : n.AtLeastTwo
⊢ ↑(OfNat.ofNat n) = OfNat.ofNat n

Tactic:
rfl

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Blocks.lean
/-- An intersection of blocks is a block. -/
@[to_additive "An intersection of blocks is a block."]
lemma IsBlock.iInter {ι : Sort*} {B : ι → Set X} (hB : ∀ i, IsBlock G (B i)) :
    IsBlock G (⋂ i, B i)

Proof state:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
ι : Sort u_3
B : ι → Set X
hB : ∀ (i : ι), IsBlock G (B i)
⊢ IsBlock G (⋂ i, B i)

Tactic:
simp only [isBlock_iff_smul_eq_smul_of_nonempty, smul_set_iInter] at hB ⊢

Result:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
ι : Sort u_3
B : ι → Set X
hB : ∀ (i : ι) ⦃g₁ g₂ : G⦄, (g₁ • B i ∩ g₂ • B i).Nonempty → g₁ • B i = g₂ • B i
⊢ ∀ ⦃g₁ g₂ : G⦄, ((⋂ i, g₁ • B i) ∩ ⋂ i, g₂ • B i).Nonempty → ⋂ i, g₁ • B i = ⋂ i, g₂ • B i

Proof state:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
ι : Sort u_3
B : ι → Set X
hB : ∀ (i : ι) ⦃g₁ g₂ : G⦄, (g₁ • B i ∩ g₂ • B i).Nonempty → g₁ • B i = g₂ • B i
⊢ ∀ ⦃g₁ g₂ : G⦄, ((⋂ i, g₁ • B i) ∩ ⋂ i, g₂ • B i).Nonempty → ⋂ i, g₁ • B i = ⋂ i, g₂ • B i

Tactic:
rintro g₁ g₂ ⟨a, ha₁, ha₂⟩

Result:
case intro.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
ι : Sort u_3
B : ι → Set X
hB : ∀ (i : ι) ⦃g₁ g₂ : G⦄, (g₁ • B i ∩ g₂ • B i).Nonempty → g₁ • B i = g₂ • B i
g₁ g₂ : G
a : X
ha₁ : a ∈ ⋂ i, g₁ • B i
ha₂ : a ∈ ⋂ i, g₂ • B i
⊢ ⋂ i, g₁ • B i = ⋂ i, g₂ • B i

Proof state:
case intro.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
ι : Sort u_3
B : ι → Set X
hB : ∀ (i : ι) ⦃g₁ g₂ : G⦄, (g₁ • B i ∩ g₂ • B i).Nonempty → g₁ • B i = g₂ • B i
g₁ g₂ : G
a : X
ha₁ : a ∈ ⋂ i, g₁ • B i
ha₂ : a ∈ ⋂ i, g₂ • B i
⊢ ⋂ i, g₁ • B i = ⋂ i, g₂ • B i

Tactic:
simp_rw [fun i ↦ hB i ⟨a, iInter_subset _ i ha₁, iInter_subset _ i ha₂⟩]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/BochnerL1.lean
theorem negPart_map_norm (f : α →ₛ ℝ) : (negPart f).map norm = negPart f

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f : α →ₛ ℝ
⊢ map norm f.negPart = f.negPart

Tactic:
rw [negPart]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
f : α →ₛ ℝ
⊢ map norm (-f).posPart = (-f).posPart

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f : α →ₛ ℝ
⊢ map norm (-f).posPart = (-f).posPart

Tactic:
exact posPart_map_norm _

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem iUnion_univ_pi {ι : α → Type*} (t : (a : α) → ι a → Set (π a)) :
    ⋃ x : (a : α) → ι a, pi univ (fun a => t a (x a)) = pi univ fun a => ⋃ j : ι a, t a j

Proof state:
α : Type u_1
π : α → Type u_12
ι : α → Type u_13
t : (a : α) → ι a → Set (π a)
⊢ (⋃ x, univ.pi fun a => t a (x a)) = univ.pi fun a => ⋃ j, t a j

Tactic:
ext

Result:
case h
α : Type u_1
π : α → Type u_12
ι : α → Type u_13
t : (a : α) → ι a → Set (π a)
x✝ : (i : α) → π i
⊢ (x✝ ∈ ⋃ x, univ.pi fun a => t a (x a)) ↔ x✝ ∈ univ.pi fun a => ⋃ j, t a j

Proof state:
case h
α : Type u_1
π : α → Type u_12
ι : α → Type u_13
t : (a : α) → ι a → Set (π a)
x✝ : (i : α) → π i
⊢ (x✝ ∈ ⋃ x, univ.pi fun a => t a (x a)) ↔ x✝ ∈ univ.pi fun a => ⋃ j, t a j

Tactic:
simp [Classical.skolem]

Result:
no goals
-- Mathlib/GroupTheory/CoprodI.lean
theorem mclosure_iUnion_range_of :
    Submonoid.closure (⋃ i, Set.range (of : M i →* CoprodI M)) = ⊤

Proof state:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
⊢ Submonoid.closure (⋃ i, range ⇑of) = ⊤

Tactic:
simp [Submonoid.closure_iUnion]

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/QuadraticReciprocity.lean
theorem exists_sq_eq_prime_iff_of_mod_four_eq_one (hp1 : p % 4 = 1) (hq1 : q ≠ 2) :
    IsSquare (q : ZMod p) ↔ IsSquare (p : ZMod q)

Proof state:
case inr
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp1 : p % 4 = 1
hq1 : q ≠ 2
h : p ≠ q
⊢ IsSquare ↑q ↔ IsSquare ↑p

Tactic:
rw [← eq_one_iff' p (prime_ne_zero p q h), ← eq_one_iff' q (prime_ne_zero q p h.symm),
  quadratic_reciprocity_one_mod_four hp1 hq1]

Result:
no goals

Proof state:
case inl
q : ℕ
inst✝¹ : Fact (Nat.Prime q)
hq1 : q ≠ 2
inst✝ : Fact (Nat.Prime q)
hp1 : q % 4 = 1
⊢ IsSquare ↑q ↔ IsSquare ↑q

Tactic:
rfl

Result:
no goals

Proof state:
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp1 : p % 4 = 1
hq1 : q ≠ 2
⊢ IsSquare ↑q ↔ IsSquare ↑p

Tactic:
rcases eq_or_ne p q with h | h

Result:
case inl
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp1 : p % 4 = 1
hq1 : q ≠ 2
h : p = q
⊢ IsSquare ↑q ↔ IsSquare ↑p

case inr
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp1 : p % 4 = 1
hq1 : q ≠ 2
h : p ≠ q
⊢ IsSquare ↑q ↔ IsSquare ↑p

Proof state:
case inl
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp1 : p % 4 = 1
hq1 : q ≠ 2
h : p = q
⊢ IsSquare ↑q ↔ IsSquare ↑p

Tactic:
subst p

Result:
case inl
q : ℕ
inst✝¹ : Fact (Nat.Prime q)
hq1 : q ≠ 2
inst✝ : Fact (Nat.Prime q)
hp1 : q % 4 = 1
⊢ IsSquare ↑q ↔ IsSquare ↑q
-- Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean
private lemma lipschitzWith_toMatrixAux :
    LipschitzWith 1 (ofMatrixₗ.symm (R := ℂ) : CStarMatrix m n A → Matrix m n A)

Proof state:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
M : CStarMatrix m n A
⊢ ‖ofMatrixₗ.symm M‖₊ ≤ 1 * ‖M‖₊

Tactic:
rw [one_mul, ← NNReal.coe_le_coe, coe_nnnorm, coe_nnnorm, Matrix.norm_le_iff (norm_nonneg _)]

Result:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
M : CStarMatrix m n A
⊢ ∀ (i : m) (j : n), ‖ofMatrixₗ.symm M i j‖ ≤ ‖M‖

Proof state:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ LipschitzWith 1 ⇑ofMatrixₗ.symm

Tactic:
refine AddMonoidHomClass.lipschitz_of_bound_nnnorm _ _ fun M => ?_

Result:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
M : CStarMatrix m n A
⊢ ‖ofMatrixₗ.symm M‖₊ ≤ 1 * ‖M‖₊

Proof state:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
M : CStarMatrix m n A
⊢ ∀ (i : m) (j : n), ‖ofMatrixₗ.symm M i j‖ ≤ ‖M‖

Tactic:
exact fun _ _ ↦ CStarMatrix.norm_entry_le_norm

Result:
no goals
-- Mathlib/RingTheory/Nilpotent/Basic.lean
theorem add_pow_add_eq_zero_of_pow_eq_zero (h_comm : Commute x y) {m n : ℕ}
    (hx : x ^ m = 0) (hy : y ^ n = 0) :
    (x + y) ^ (m + n - 1) = 0 :=
  h_comm.add_pow_eq_zero_of_add_le_succ_of_pow_eq_zero hx hy <| by rw [← Nat.sub_le_iff_le_add]

Proof state:
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
m n : ℕ
hx : x ^ m = 0
hy : y ^ n = 0
⊢ m + n ≤ m + n - 1 + 1

Tactic:
rw [← Nat.sub_le_iff_le_add]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MapComap.lean
@[simp]
lemma comap_zero (hg : Measurable g) : Kernel.comap (0 : Kernel α β) g hg = 0

Proof state:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
g : γ → α
hg : Measurable g
a✝¹ : γ
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((comap 0 g hg) a✝¹) s✝ = (0 a✝¹) s✝

Tactic:
rw [Kernel.comap_apply]

Result:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
g : γ → α
hg : Measurable g
a✝¹ : γ
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ (0 (g a✝¹)) s✝ = (0 a✝¹) s✝

Proof state:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
g : γ → α
hg : Measurable g
a✝¹ : γ
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ (0 (g a✝¹)) s✝ = (0 a✝¹) s✝

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
g : γ → α
hg : Measurable g
⊢ comap 0 g hg = 0

Tactic:
ext

Result:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
g : γ → α
hg : Measurable g
a✝¹ : γ
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((comap 0 g hg) a✝¹) s✝ = (0 a✝¹) s✝
-- Mathlib/Algebra/Algebra/Quasispectrum.lean
lemma quasispectrum_eq_spectrum_inr (R : Type*) {A : Type*} [CommRing R] [NonUnitalRing A]
    [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (a : A) :
    quasispectrum R a = spectrum R (a : Unitization R A)

Proof state:
case h
R : Type u_3
A : Type u_4
inst✝⁴ : CommRing R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a : A
r : R
this : {r | ¬IsUnit r} ⊆ spectrum R ↑a
⊢ r ∈ quasispectrum R a ↔ r ∈ quasispectrum R ↑a

Tactic:
apply forall_congr' fun hr ↦ ?_

Result:
R : Type u_3
A : Type u_4
inst✝⁴ : CommRing R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a : A
r : R
this : {r | ¬IsUnit r} ⊆ spectrum R ↑a
hr : IsUnit r
⊢ ¬IsQuasiregular (-(hr.unit⁻¹ • a)) ↔ ¬IsQuasiregular (-(hr.unit⁻¹ • ↑a))

Proof state:
R : Type u_3
A : Type u_4
inst✝⁴ : CommRing R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a : A
r : R
this : {r | ¬IsUnit r} ⊆ spectrum R ↑a
hr : IsUnit r
⊢ ¬IsQuasiregular (-(hr.unit⁻¹ • a)) ↔ ¬IsQuasiregular (-(hr.unit⁻¹ • ↑a))

Tactic:
rw [not_iff_not, Units.smul_def, Units.smul_def, ← inr_smul, ← inr_neg, isQuasiregular_inr_iff]

Result:
no goals

Proof state:
R : Type u_3
A : Type u_4
inst✝⁴ : CommRing R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a : A
⊢ quasispectrum R a = spectrum R ↑a

Tactic:
ext r

Result:
case h
R : Type u_3
A : Type u_4
inst✝⁴ : CommRing R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a : A
r : R
⊢ r ∈ quasispectrum R a ↔ r ∈ spectrum R ↑a

Proof state:
case h
R : Type u_3
A : Type u_4
inst✝⁴ : CommRing R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a : A
r : R
this : {r | ¬IsUnit r} ⊆ spectrum R ↑a
⊢ r ∈ quasispectrum R a ↔ r ∈ spectrum R ↑a

Tactic:
rw [← Set.union_eq_left.mpr this, ← quasispectrum_eq_spectrum_union]

Result:
case h
R : Type u_3
A : Type u_4
inst✝⁴ : CommRing R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a : A
r : R
this : {r | ¬IsUnit r} ⊆ spectrum R ↑a
⊢ r ∈ quasispectrum R a ↔ r ∈ quasispectrum R ↑a

Proof state:
case h
R : Type u_3
A : Type u_4
inst✝⁴ : CommRing R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a : A
r : R
⊢ r ∈ quasispectrum R a ↔ r ∈ spectrum R ↑a

Tactic:
have : { r | ¬ IsUnit r} ⊆ spectrum R _ := mem_spectrum_inr_of_not_isUnit a

Result:
case h
R : Type u_3
A : Type u_4
inst✝⁴ : CommRing R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a : A
r : R
this : {r | ¬IsUnit r} ⊆ spectrum R ↑a
⊢ r ∈ quasispectrum R a ↔ r ∈ spectrum R ↑a
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem mex_monotone {α β : Type u} {f : α → Ordinal.{max u v}} {g : β → Ordinal.{max u v}}
    (h : Set.range f ⊆ Set.range g) : mex.{_, v} f ≤ mex.{_, v} g

Proof state:
α β : Type u
f : α → Ordinal.{max u v}
g : β → Ordinal.{max u v}
h : range f ⊆ range g
i : α
hi : f i = mex g
⊢ False

Tactic:
obtain ⟨j, hj⟩ := h ⟨i, rfl⟩

Result:
case intro
α β : Type u
f : α → Ordinal.{max u v}
g : β → Ordinal.{max u v}
h : range f ⊆ range g
i : α
hi : f i = mex g
j : β
hj : g j = f i
⊢ False

Proof state:
case intro
α β : Type u
f : α → Ordinal.{max u v}
g : β → Ordinal.{max u v}
h : range f ⊆ range g
i : α
j : β
hi : g j = mex g
hj : g j = f i
⊢ False

Tactic:
exact ne_mex g j hi

Result:
no goals

Proof state:
α β : Type u
f : α → Ordinal.{max u v}
g : β → Ordinal.{max u v}
h : range f ⊆ range g
⊢ mex f ≤ mex g

Tactic:
refine mex_le_of_ne fun i hi => ?_

Result:
α β : Type u
f : α → Ordinal.{max u v}
g : β → Ordinal.{max u v}
h : range f ⊆ range g
i : α
hi : f i = mex g
⊢ False

Proof state:
case intro
α β : Type u
f : α → Ordinal.{max u v}
g : β → Ordinal.{max u v}
h : range f ⊆ range g
i : α
hi : f i = mex g
j : β
hj : g j = f i
⊢ False

Tactic:
rw [← hj] at hi

Result:
case intro
α β : Type u
f : α → Ordinal.{max u v}
g : β → Ordinal.{max u v}
h : range f ⊆ range g
i : α
j : β
hi : g j = mex g
hj : g j = f i
⊢ False
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem zip_eq_nil_iff {l₁ : List α} {l₂ : List β} :
    zip l₁ l₂ = [] ↔ l₁ = [] ∨ l₂ = []

Proof state:
α : Type u_1
β : Type u_2
l₁ : List α
l₂ : List β
⊢ l₁.zip l₂ = [] ↔ l₁ = [] ∨ l₂ = []

Tactic:
simp [zip_eq_zipWith]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Inversion/ImageHyperplane.lean
theorem image_inversion_perpBisector (hR : R ≠ 0) (hy : y ≠ c) :
    inversion c R '' perpBisector c y = sphere (inversion c R y) (R ^ 2 / dist y c) \ {c}

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
⊢ inversion c R '' ↑(perpBisector c y) = sphere (inversion c R y) (R ^ 2 / dist y c) \ {c}

Tactic:
rw [image_eq_preimage_of_inverse (inversion_involutive _ hR) (inversion_involutive _ hR),
  preimage_inversion_perpBisector hR hy]

Result:
no goals
-- Mathlib/Data/Real/Sign.lean
theorem sign_eq_zero_iff {r : ℝ} : sign r = 0 ↔ r = 0

Proof state:
case inl
r : ℝ
h : r.sign = 0
hn : r < 0
⊢ r = 0

Tactic:
rw [sign_of_neg hn, neg_eq_zero] at h

Result:
case inl
r : ℝ
h : 1 = 0
hn : r < 0
⊢ r = 0

Proof state:
r : ℝ
⊢ r.sign = 0 ↔ r = 0

Tactic:
refine ⟨fun h => ?_, fun h => h.symm ▸ sign_zero⟩

Result:
r : ℝ
h : r.sign = 0
⊢ r = 0

Proof state:
case inr.inr
r : ℝ
h : r.sign = 0
hp : 0 < r
⊢ r = 0

Tactic:
rw [sign_of_pos hp] at h

Result:
case inr.inr
r : ℝ
h : 1 = 0
hp : 0 < r
⊢ r = 0

Proof state:
case inl
r : ℝ
h : 1 = 0
hn : r < 0
⊢ r = 0

Tactic:
exact (one_ne_zero h).elim

Result:
no goals

Proof state:
r : ℝ
h : r.sign = 0
⊢ r = 0

Tactic:
obtain hn | rfl | hp := lt_trichotomy r (0 : ℝ)

Result:
case inl
r : ℝ
h : r.sign = 0
hn : r < 0
⊢ r = 0

case inr.inl
h : sign 0 = 0
⊢ 0 = 0

case inr.inr
r : ℝ
h : r.sign = 0
hp : 0 < r
⊢ r = 0

Proof state:
case inr.inl
h : sign 0 = 0
⊢ 0 = 0

Tactic:
rfl

Result:
no goals

Proof state:
case inr.inr
r : ℝ
h : 1 = 0
hp : 0 < r
⊢ r = 0

Tactic:
exact (one_ne_zero h).elim

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Preorder/HasIterationOfShape.lean
lemma hasColimitsOfShape_of_isSuccLimit'
    {α : Type*} [PartialOrder α] (h : α <i J) (hα : Order.IsSuccLimit h.top) :
    HasColimitsOfShape α C

Proof state:
J : Type w
inst✝³ : LinearOrder J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasIterationOfShape J C
α : Type u_1
inst✝ : PartialOrder α
h : (fun x1 x2 => x1 < x2) ≺i fun x1 x2 => x1 < x2
hα : Order.IsSuccLimit h.top
this : HasColimitsOfShape (↑(Set.Iio h.top)) C
⊢ HasColimitsOfShape α C

Tactic:
exact hasColimitsOfShape_of_equivalence h.orderIsoIio.equivalence.symm

Result:
no goals

Proof state:
J : Type w
inst✝³ : LinearOrder J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasIterationOfShape J C
α : Type u_1
inst✝ : PartialOrder α
h : (fun x1 x2 => x1 < x2) ≺i fun x1 x2 => x1 < x2
hα : Order.IsSuccLimit h.top
⊢ HasColimitsOfShape α C

Tactic:
have := hasColimitsOfShape_of_isSuccLimit C h.top hα

Result:
J : Type w
inst✝³ : LinearOrder J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasIterationOfShape J C
α : Type u_1
inst✝ : PartialOrder α
h : (fun x1 x2 => x1 < x2) ≺i fun x1 x2 => x1 < x2
hα : Order.IsSuccLimit h.top
this : HasColimitsOfShape (↑(Set.Iio h.top)) C
⊢ HasColimitsOfShape α C
-- Mathlib/Data/List/Chain.lean
theorem Chain.pairwise [IsTrans α R] :
    ∀ {a : α} {l : List α}, Chain R a l → Pairwise R (a :: l)
  | _, [], Chain.nil => pairwise_singleton _ _
  | a, _, @Chain.cons _ _ _ b l h hb =>
    hb.pairwise.cons
      (by
        simp only [mem_cons, forall_eq_or_imp, h, true_and]
        exact fun c hc => _root_.trans h (rel_of_pairwise_cons hb.pairwise hc))

Proof state:
α : Type u
R : α → α → Prop
inst✝ : IsTrans α R
a b : α
l : List α
h : R a b
hb : Chain R b l
⊢ ∀ (a_1 : α), a_1 ∈ l → R a a_1

Tactic:
exact fun c hc => _root_.trans h (rel_of_pairwise_cons hb.pairwise hc)

Result:
no goals

Proof state:
α : Type u
R : α → α → Prop
inst✝ : IsTrans α R
a b : α
l : List α
h : R a b
hb : Chain R b l
⊢ ∀ (a' : α), a' ∈ b :: l → R a a'

Tactic:
simp only [mem_cons, forall_eq_or_imp, h, true_and]

Result:
α : Type u
R : α → α → Prop
inst✝ : IsTrans α R
a b : α
l : List α
h : R a b
hb : Chain R b l
⊢ ∀ (a_1 : α), a_1 ∈ l → R a a_1
-- Mathlib/Analysis/InnerProductSpace/Defs.lean
theorem inner_sub_right (x y z : F) : ⟪x, y - z⟫ = ⟪x, y⟫ - ⟪x, z⟫

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y z : F
⊢ ⟪x, y - z⟫_𝕜 = ⟪x, y⟫_𝕜 - ⟪x, z⟫_𝕜

Tactic:
simp [sub_eq_add_neg, inner_add_right, inner_neg_right]

Result:
no goals
-- Mathlib/Topology/Algebra/Module/Multilinear/Basic.lean
theorem _root_.ContinuousLinearMap.compContinuousMultilinearMap_coe (g : M₂ →L[R] M₃)
    (f : ContinuousMultilinearMap R M₁ M₂) :
    (g.compContinuousMultilinearMap f : (∀ i, M₁ i) → M₃) =
      (g : M₂ → M₃) ∘ (f : (∀ i, M₁ i) → M₂)

Proof state:
R : Type u
ι : Type v
M₁ : ι → Type w₁
M₂ : Type w₂
M₃ : Type w₃
inst✝⁹ : Semiring R
inst✝⁸ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : (i : ι) → Module R (M₁ i)
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
inst✝² : (i : ι) → TopologicalSpace (M₁ i)
inst✝¹ : TopologicalSpace M₂
inst✝ : TopologicalSpace M₃
g : M₂ →L[R] M₃
f : ContinuousMultilinearMap R M₁ M₂
⊢ ⇑(g.compContinuousMultilinearMap f) = ⇑g ∘ ⇑f

Tactic:
ext m

Result:
case h
R : Type u
ι : Type v
M₁ : ι → Type w₁
M₂ : Type w₂
M₃ : Type w₃
inst✝⁹ : Semiring R
inst✝⁸ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : (i : ι) → Module R (M₁ i)
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
inst✝² : (i : ι) → TopologicalSpace (M₁ i)
inst✝¹ : TopologicalSpace M₂
inst✝ : TopologicalSpace M₃
g : M₂ →L[R] M₃
f : ContinuousMultilinearMap R M₁ M₂
m : (i : ι) → M₁ i
⊢ (g.compContinuousMultilinearMap f) m = (⇑g ∘ ⇑f) m

Proof state:
case h
R : Type u
ι : Type v
M₁ : ι → Type w₁
M₂ : Type w₂
M₃ : Type w₃
inst✝⁹ : Semiring R
inst✝⁸ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : (i : ι) → Module R (M₁ i)
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
inst✝² : (i : ι) → TopologicalSpace (M₁ i)
inst✝¹ : TopologicalSpace M₂
inst✝ : TopologicalSpace M₃
g : M₂ →L[R] M₃
f : ContinuousMultilinearMap R M₁ M₂
m : (i : ι) → M₁ i
⊢ (g.compContinuousMultilinearMap f) m = (⇑g ∘ ⇑f) m

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
lemma inner_eq_zero_of_left {x : E} (y : E) (h : ‖x‖ = 0) : ⟪x, y⟫_𝕜 = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h : ‖x‖ = 0
⊢ ‖⟪x, y⟫_𝕜‖ = 0

Tactic:
refine le_antisymm ?_ (by positivity)

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h : ‖x‖ = 0
⊢ ‖⟪x, y⟫_𝕜‖ ≤ 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h : ‖x‖ = 0
⊢ ‖x‖ * ‖y‖ ≤ 0

Tactic:
simp [h]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h : ‖x‖ = 0
⊢ 0 ≤ ‖⟪x, y⟫_𝕜‖

Tactic:
positivity

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h : ‖x‖ = 0
⊢ ⟪x, y⟫_𝕜 = 0

Tactic:
rw [← norm_eq_zero]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h : ‖x‖ = 0
⊢ ‖⟪x, y⟫_𝕜‖ = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h : ‖x‖ = 0
⊢ ‖⟪x, y⟫_𝕜‖ ≤ 0

Tactic:
exact norm_inner_le_norm _ _ |>.trans <| by simp [h]

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/EpiMono.lean
theorem mono_iff_injective : Mono f ↔ Function.Injective f

Proof state:
R : Type u
inst✝ : Ring R
X Y : ModuleCat R
f : X ⟶ Y
⊢ Mono f ↔ Function.Injective ⇑(ConcreteCategory.hom f)

Tactic:
rw [mono_iff_ker_eq_bot, LinearMap.ker_eq_bot]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Icc_eq_Ico_same_iff : Icc a b = Ico a b ↔ ¬a ≤ b where
  mp h

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
h : ¬a ≤ b
⊢ Icc a b = Ico a b

Tactic:
rw [Icc_eq_empty h, Ico_eq_empty (mt le_of_lt h)]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
h : Icc a b = Ico a b
⊢ ¬a ≤ b

Tactic:
simpa using Set.ext_iff.mp h b

Result:
no goals
-- Mathlib/Algebra/Group/Indicator.lean
theorem mulIndicator_apply (s : Set α) (f : α → M) (a : α) [Decidable (a ∈ s)] :
    mulIndicator s f a = if a ∈ s then f a else 1

Proof state:
α : Type u_1
M : Type u_3
inst✝¹ : One M
s : Set α
f : α → M
a : α
inst✝ : Decidable (a ∈ s)
⊢ s.mulIndicator f a = if a ∈ s then f a else 1

Tactic:
unfold mulIndicator

Result:
α : Type u_1
M : Type u_3
inst✝¹ : One M
s : Set α
f : α → M
a : α
inst✝ : Decidable (a ∈ s)
⊢ (if a ∈ s then f a else 1) = if a ∈ s then f a else 1

Proof state:
α : Type u_1
M : Type u_3
inst✝¹ : One M
s : Set α
f : α → M
a : α
inst✝ : Decidable (a ∈ s)
⊢ (if a ∈ s then f a else 1) = if a ∈ s then f a else 1

Tactic:
congr

Result:
no goals
-- Mathlib/RingTheory/Ideal/Quotient/Defs.lean
theorem factor_comp_apply (H1 : S ≤ T) (H2 : T ≤ U) (x : R ⧸ S) :
    factor H2 (factor H1 x) = factor (H1.trans H2) x

Proof state:
R : Type u
inst✝³ : Ring R
S T U : Ideal R
inst✝² : S.IsTwoSided
inst✝¹ : T.IsTwoSided
inst✝ : U.IsTwoSided
H1 : S ≤ T
H2 : T ≤ U
x : R ⧸ S
⊢ (factor H2) ((factor H1) x) = (factor ⋯) x

Tactic:
rw [← RingHom.comp_apply]

Result:
R : Type u
inst✝³ : Ring R
S T U : Ideal R
inst✝² : S.IsTwoSided
inst✝¹ : T.IsTwoSided
inst✝ : U.IsTwoSided
H1 : S ≤ T
H2 : T ≤ U
x : R ⧸ S
⊢ ((factor H2).comp (factor H1)) x = (factor ⋯) x

Proof state:
R : Type u
inst✝³ : Ring R
S T U : Ideal R
inst✝² : S.IsTwoSided
inst✝¹ : T.IsTwoSided
inst✝ : U.IsTwoSided
H1 : S ≤ T
H2 : T ≤ U
x : R ⧸ S
⊢ ((factor H2).comp (factor H1)) x = (factor ⋯) x

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem bmod_add_cancel (x : Int) (n : Nat) : Int.bmod (x + n) n = Int.bmod x n

Proof state:
x : Int
n : Nat
⊢ (x + ↑n).bmod n = x.bmod n

Tactic:
simp [bmod_def]

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem hausdorffDist_closure : hausdorffDist (closure s) (closure t) = hausdorffDist s t

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
⊢ hausdorffDist (closure s) (closure t) = hausdorffDist s t

Tactic:
simp [hausdorffDist]

Result:
no goals