harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem Decidable.and_or_imp [Decidable a] : a ∧ b ∨ (a → c) ↔ a → b ∨ c :=
  if ha : a then by simp only [ha, true_and, true_imp_iff]
  else by simp only [ha, false_or, false_and, false_imp_iff]

Proof state:
a b c : Prop
inst✝ : Decidable a
ha : ¬a
⊢ a ∧ b ∨ (a → c) ↔ a → b ∨ c

Tactic:
simp only [ha, false_or, false_and, false_imp_iff]

Result:
no goals

Proof state:
a b c : Prop
inst✝ : Decidable a
ha : a
⊢ a ∧ b ∨ (a → c) ↔ a → b ∨ c

Tactic:
simp only [ha, true_and, true_imp_iff]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem all_eq (s : String) (p : Char → Bool) : all s p = s.1.all p

Proof state:
s : String
p : Char → Bool
⊢ s.all p = s.data.all p

Tactic:
rw [all, any_eq, List.all_eq_not_any_not]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCofiber.lean
@[reassoc (attr := simp)]
lemma inlX_π (i j : ι) (hij : c.Rel j i) :
    inlX K i j hij ≫ (π K).f j = 0

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Preadditive C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : HasHomotopyCofiber (biprod.lift (𝟙 K) (-𝟙 K))
i j : ι
hij : c.Rel j i
⊢ ((Homotopy.ofEq ⋯).trans (Homotopy.equivSubZero (Homotopy.refl (𝟙 K)))).hom i j = 0

Tactic:
simp [Homotopy.equivSubZero]

Result:
no goals

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Preadditive C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : HasHomotopyCofiber (biprod.lift (𝟙 K) (-𝟙 K))
i j : ι
hij : c.Rel j i
⊢ inlX K i j hij ≫ (π K).f j = 0

Tactic:
erw [homotopyCofiber.inlX_desc_f]

Result:
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Preadditive C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : HasHomotopyCofiber (biprod.lift (𝟙 K) (-𝟙 K))
i j : ι
hij : c.Rel j i
⊢ ((Homotopy.ofEq ⋯).trans (Homotopy.equivSubZero (Homotopy.refl (𝟙 K)))).hom i j = 0
-- Mathlib/Analysis/Convex/Side.lean
theorem wOppSide_smul_vsub_vadd_left {s : AffineSubspace R P} {p₁ p₂ : P} (x : P) (hp₁ : p₁ ∈ s)
    (hp₂ : p₂ ∈ s) {t : R} (ht : t ≤ 0) : s.WOppSide (t • (x -ᵥ p₁) +ᵥ p₂) x

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
p₁ p₂ x : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : t ≤ 0
⊢ s.WOppSide (t • (x -ᵥ p₁) +ᵥ p₂) x

Tactic:
refine ⟨p₂, hp₂, p₁, hp₁, ?_⟩

Result:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
p₁ p₂ x : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : t ≤ 0
⊢ SameRay R ((t • (x -ᵥ p₁) +ᵥ p₂) -ᵥ p₂) (p₁ -ᵥ x)

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
p₁ p₂ x : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : t ≤ 0
⊢ SameRay R ((t • (x -ᵥ p₁) +ᵥ p₂) -ᵥ p₂) (p₁ -ᵥ x)

Tactic:
rw [vadd_vsub, ← neg_neg t, neg_smul, ← smul_neg, neg_vsub_eq_vsub_rev]

Result:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
p₁ p₂ x : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : t ≤ 0
⊢ SameRay R (-t • (p₁ -ᵥ x)) (p₁ -ᵥ x)

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
p₁ p₂ x : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : t ≤ 0
⊢ SameRay R (-t • (p₁ -ᵥ x)) (p₁ -ᵥ x)

Tactic:
exact SameRay.sameRay_nonneg_smul_left _ (neg_nonneg.2 ht)

Result:
no goals
-- Mathlib/Data/Nat/Choose/Basic.lean
theorem multichoose_one_right (n : ℕ) : multichoose n 1 = n

Proof state:
n : ℕ
⊢ n.multichoose 1 = n

Tactic:
induction' n with n IH

Result:
case zero

⊢ multichoose 0 1 = 0

case succ
n : ℕ
IH : n.multichoose 1 = n
⊢ (n + 1).multichoose 1 = n + 1

Proof state:
case succ
n : ℕ
IH : n.multichoose 1 = n
⊢ (n + 1).multichoose 1 = n + 1

Tactic:
simp [multichoose_succ_succ n 0, IH]

Result:
no goals

Proof state:
case zero

⊢ multichoose 0 1 = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem mem_head?_append_of_mem_head? {s t : List α} {x : α} (h : x ∈ s.head?) :
    x ∈ (s ++ t).head?

Proof state:
case cons
α : Type u
t : List α
x head✝ : α
tail✝ : List α
h : x ∈ (head✝ :: tail✝).head?
⊢ x ∈ (head✝ :: tail✝ ++ t).head?

Tactic:
exact h

Result:
no goals

Proof state:
α : Type u
s t : List α
x : α
h : x ∈ s.head?
⊢ x ∈ (s ++ t).head?

Tactic:
cases s

Result:
case nil
α : Type u
t : List α
x : α
h : x ∈ [].head?
⊢ x ∈ ([] ++ t).head?

case cons
α : Type u
t : List α
x head✝ : α
tail✝ : List α
h : x ∈ (head✝ :: tail✝).head?
⊢ x ∈ (head✝ :: tail✝ ++ t).head?

Proof state:
case nil
α : Type u
t : List α
x : α
h : x ∈ [].head?
⊢ x ∈ ([] ++ t).head?

Tactic:
contradiction

Result:
no goals
-- Mathlib/Data/Vector/MapLemmas.lean
theorem mapAccumr₂_mapAccumr₂_left_right
    (f₁ : γ → β → σ₁ → σ₁ × φ) (f₂ : α → β → σ₂ → σ₂ × γ) :
    (mapAccumr₂ f₁ (mapAccumr₂ f₂ xs ys s₂).snd ys s₁)
    = let m := mapAccumr₂ (fun x y (s₁, s₂) =>
                let r₂ := f₂ x y s₂
                let r₁ := f₁ r₂.snd y s₁
                ((r₁.fst, r₂.fst), r₁.snd)
              )
            xs ys (s₁, s₂)
    (m.fst.fst, m.snd)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
φ : Type u_8
n : ℕ
s₁ : σ₁
s₂ : σ₂
xs : Vector α n
ys : Vector β n
f₁ : γ → β → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
⊢ mapAccumr₂ f₁ (mapAccumr₂ f₂ xs ys s₂).2 ys s₁ =
    let m :=
      mapAccumr₂
        (fun x y x_1 =>
          match x_1 with
          | (s₁, s₂) =>
            let r₂ := f₂ x y s₂;
            let r₁ := f₁ r₂.2 y s₁;
            ((r₁.1, r₂.1), r₁.2))
        xs ys (s₁, s₂);
    (m.1.1, m.2)

Tactic:
induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂ <;> simp_all

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
theorem lt_mul_of_one_lt_right [PosMulStrictMono α] (ha : 0 < a) (h : 1 < b) : a < a * b

Proof state:
α : Type u_3
a b : α
inst✝³ : MulOneClass α
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
ha : 0 < a
h : 1 < b
⊢ a < a * b

Tactic:
simpa only [mul_one] using mul_lt_mul_of_pos_left h ha

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Transvection.lean
theorem mul_transvection_apply_same (a : n) (c : R) (M : Matrix n n R) :
    (M * transvection i j c) a j = M a j + c * M a i

Proof state:
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
i j : n
inst✝ : Fintype n
a : n
c : R
M : Matrix n n R
⊢ (M * transvection i j c) a j = M a j + c * M a i

Tactic:
simp [transvection, Matrix.mul_add, mul_comm]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
theorem iteratedFDerivWithin_insert {n y} :
    iteratedFDerivWithin 𝕜 n f (insert x s) y = iteratedFDerivWithin 𝕜 n f s y :=
  iteratedFDerivWithin_congr_set' (y := x)
    (eventually_mem_nhdsWithin.mono <| by intros; simp_all).set_eq _

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ
y x✝ : E
a✝ : x✝ ∈ {x}ᶜ
⊢ x✝ ∈ insert x s ↔ x✝ ∈ s

Tactic:
simp_all

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ
y : E
⊢ ∀ x_1 ∈ {x}ᶜ, x_1 ∈ insert x s ↔ x_1 ∈ s

Tactic:
intros

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ
y x✝ : E
a✝ : x✝ ∈ {x}ᶜ
⊢ x✝ ∈ insert x s ↔ x✝ ∈ s
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem mem_closure_iff_infEdist_zero : x ∈ closure s ↔ infEdist x s = 0 :=
  ⟨fun h => by
    rw [← infEdist_closure]
    exact infEdist_zero_of_mem h,
   fun h =>
    EMetric.mem_closure_iff.2 fun ε εpos => infEdist_lt_iff.mp <| by rwa [h]⟩

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
h : x ∈ closure s
⊢ infEdist x s = 0

Tactic:
rw [← infEdist_closure]

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
h : x ∈ closure s
⊢ infEdist x (closure s) = 0

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
h : infEdist x s = 0
ε : ℝ≥0∞
εpos : ε > 0
⊢ infEdist x s < ε

Tactic:
rwa [h]

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
h : x ∈ closure s
⊢ infEdist x (closure s) = 0

Tactic:
exact infEdist_zero_of_mem h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getLast_eq_iff_getLast?_eq_some {xs : List α} (h) :
    xs.getLast h = a ↔ xs.getLast? = some a

Proof state:
α : Type u_1
a : α
xs : List α
h : xs ≠ []
⊢ xs.getLast h = a ↔ xs.getLast? = some a

Tactic:
rw [getLast?_eq_getLast _ h]

Result:
α : Type u_1
a : α
xs : List α
h : xs ≠ []
⊢ xs.getLast h = a ↔ some (xs.getLast h) = some a

Proof state:
α : Type u_1
a : α
xs : List α
h : xs ≠ []
⊢ xs.getLast h = a ↔ some (xs.getLast h) = some a

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Matrix/Hadamard.lean
theorem stdBasisMatrix_hadamard_stdBasisMatrix_of_ne
    {ia : m} {ja : n} {ib : m} {jb : n} (h : ¬(ia = ib ∧ ja = jb)) (a b : α) :
    stdBasisMatrix ia ja a ⊙ stdBasisMatrix ib jb b = 0

Proof state:
case inr
α : Type u_1
m : Type u_2
n : Type u_3
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : MulZeroClass α
ia : m
ja : n
ib : m
jb : n
a b : α
h✝ : ¬ja = jb
⊢ stdBasisMatrix ia ja a ⊙ stdBasisMatrix ib jb b = 0

Tactic:
simp only [stdBasisMatrix]

Result:
case inr
α : Type u_1
m : Type u_2
n : Type u_3
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : MulZeroClass α
ia : m
ja : n
ib : m
jb : n
a b : α
h✝ : ¬ja = jb
⊢ ((of fun i' j' => if ia = i' ∧ ja = j' then a else 0) ⊙ of fun i' j' => if ib = i' ∧ jb = j' then b else 0) = 0

Proof state:
α : Type u_1
m : Type u_2
n : Type u_3
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : MulZeroClass α
ia : m
ja : n
ib : m
jb : n
h : ¬(ia = ib ∧ ja = jb)
a b : α
⊢ stdBasisMatrix ia ja a ⊙ stdBasisMatrix ib jb b = 0

Tactic:
rw [not_and_or] at h

Result:
α : Type u_1
m : Type u_2
n : Type u_3
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : MulZeroClass α
ia : m
ja : n
ib : m
jb : n
h : ¬ia = ib ∨ ¬ja = jb
a b : α
⊢ stdBasisMatrix ia ja a ⊙ stdBasisMatrix ib jb b = 0

Proof state:
α : Type u_1
m : Type u_2
n : Type u_3
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : MulZeroClass α
ia : m
ja : n
ib : m
jb : n
h : ¬ia = ib ∨ ¬ja = jb
a b : α
⊢ stdBasisMatrix ia ja a ⊙ stdBasisMatrix ib jb b = 0

Tactic:
cases h <;> (simp only [stdBasisMatrix]; aesop)

Result:
no goals

Proof state:
case inr
α : Type u_1
m : Type u_2
n : Type u_3
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : MulZeroClass α
ia : m
ja : n
ib : m
jb : n
a b : α
h✝ : ¬ja = jb
⊢ ((of fun i' j' => if ia = i' ∧ ja = j' then a else 0) ⊙ of fun i' j' => if ib = i' ∧ jb = j' then b else 0) = 0

Tactic:
aesop

Result:
no goals
-- Mathlib/RingTheory/Localization/FractionRing.lean
theorem nontrivial (R S : Type*) [CommRing R] [Nontrivial R] [CommRing S] [Algebra R S]
    [IsFractionRing R S] : Nontrivial S

Proof state:
case h.a
R : Type u_8
S : Type u_9
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsFractionRing R S
h : ?x = ?y
⊢ 0 = 1

Tactic:
exact
  IsLocalization.injective S (le_of_eq rfl)
    (((algebraMap R S).map_zero.trans h).trans (algebraMap R S).map_one.symm)

Result:
no goals

Proof state:
case h
R : Type u_8
S : Type u_9
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsFractionRing R S
⊢ ?x ≠ ?y

Tactic:
intro h

Result:
case h
R : Type u_8
S : Type u_9
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsFractionRing R S
h : ?x = ?y
⊢ False

Proof state:
case h
R : Type u_8
S : Type u_9
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsFractionRing R S
h : ?x = ?y
⊢ False

Tactic:
apply @zero_ne_one R

Result:
case h.a
R : Type u_8
S : Type u_9
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsFractionRing R S
h : ?x = ?y
⊢ 0 = 1

Proof state:
R : Type u_8
S : Type u_9
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsFractionRing R S
⊢ Nontrivial S

Tactic:
apply nontrivial_of_ne

Result:
case h
R : Type u_8
S : Type u_9
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsFractionRing R S
⊢ ?x ≠ ?y

case x
R : Type u_8
S : Type u_9
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsFractionRing R S
⊢ S

case y
R : Type u_8
S : Type u_9
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsFractionRing R S
⊢ S
-- Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean
lemma ExactAt.isZero_homology [K.HasHomology i] (h : K.ExactAt i) :
    IsZero (K.homology i)

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
h : K.ExactAt i
⊢ IsZero (K.homology i)

Tactic:
rwa [← exactAt_iff_isZero_homology]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Util.lean
theorem nestedProof_congr (p q : Prop) (h : p = q) (hp : p) (hq : q) : HEq (@nestedProof p hp) (@nestedProof q hq)

Proof state:
p : Prop
hp hq : p
⊢ HEq ⋯ ⋯

Tactic:
apply HEq.refl

Result:
no goals

Proof state:
p q : Prop
h : p = q
hp : p
hq : q
⊢ HEq ⋯ ⋯

Tactic:
subst h

Result:
p : Prop
hp hq : p
⊢ HEq ⋯ ⋯
-- Mathlib/Data/List/Basic.lean
theorem foldl_eq_of_comm' : ∀ a b l, foldl f a (b :: l) = f (foldl f a l) b
  | _, _, [] => rfl
  | a, b, c :: l => by rw [foldl, foldl, foldl, ← foldl_eq_of_comm' .., foldl, hf]

Proof state:
α : Type u
β : Type v
f : α → β → α
hf : ∀ (a : α) (b c : β), f (f a b) c = f (f a c) b
a : α
b c : β
l : List β
⊢ foldl f a (b :: c :: l) = f (foldl f a (c :: l)) b

Tactic:
rw [foldl, foldl, foldl, ← foldl_eq_of_comm' .., foldl, hf]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem any (f) : ∀ {s}, Valid s → s.any f = s.toString.1.any f
  | _, h => let ⟨_, _, _, h⟩ := h.validFor; by simp [h.any, h.toString]

Proof state:
f : Char → Bool
x✝ : Substring
h✝ : x✝.Valid
w✝² w✝¹ w✝ : List Char
h : ValidFor w✝² w✝¹ w✝ x✝
⊢ x✝.any f = x✝.toString.data.any f

Tactic:
simp [h.any, h.toString]

Result:
no goals
-- Mathlib/Algebra/Regular/Basic.lean
theorem IsLeftRegular.ne_zero [Nontrivial R] (la : IsLeftRegular a) : a ≠ 0

Proof state:
case intro.intro
R : Type u_1
inst✝¹ : MulZeroClass R
inst✝ : Nontrivial R
la : IsLeftRegular 0
x y : R
xy : x ≠ y
⊢ 0 * x = 0 * y

Tactic:
rw [zero_mul, zero_mul]

Result:
no goals

Proof state:
case intro.intro
R : Type u_1
inst✝¹ : MulZeroClass R
inst✝ : Nontrivial R
la : IsLeftRegular 0
x y : R
xy : x ≠ y
⊢ False

Tactic:
refine xy (la (?_ : 0 * x = 0 * y))

Result:
case intro.intro
R : Type u_1
inst✝¹ : MulZeroClass R
inst✝ : Nontrivial R
la : IsLeftRegular 0
x y : R
xy : x ≠ y
⊢ 0 * x = 0 * y

Proof state:
R : Type u_1
inst✝¹ : MulZeroClass R
a : R
inst✝ : Nontrivial R
la : IsLeftRegular a
⊢ a ≠ 0

Tactic:
rintro rfl

Result:
R : Type u_1
inst✝¹ : MulZeroClass R
inst✝ : Nontrivial R
la : IsLeftRegular 0
⊢ False

Proof state:
R : Type u_1
inst✝¹ : MulZeroClass R
inst✝ : Nontrivial R
la : IsLeftRegular 0
⊢ False

Tactic:
rcases exists_pair_ne R with ⟨x, y, xy⟩

Result:
case intro.intro
R : Type u_1
inst✝¹ : MulZeroClass R
inst✝ : Nontrivial R
la : IsLeftRegular 0
x y : R
xy : x ≠ y
⊢ False
-- Mathlib/CategoryTheory/Sites/Plus.lean
theorem plusMap_comp {P Q R : Cᵒᵖ ⥤ D} (η : P ⟶ Q) (γ : Q ⟶ R) :
    J.plusMap (η ≫ γ) = J.plusMap η ≫ J.plusMap γ

Proof state:
case w.h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
x✝ : Cᵒᵖ
S : (J.Cover (unop x✝))ᵒᵖ
⊢ colimit.ι (J.diagram P (unop x✝)) S ≫ (J.plusMap (η ≫ γ)).app x✝ =
    colimit.ι (J.diagram P (unop x✝)) S ≫ (J.plusMap η ≫ J.plusMap γ).app x✝

Tactic:
simp [plusMap, J.diagramNatTrans_comp]

Result:
no goals

Proof state:
case w.h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
x✝ : Cᵒᵖ
⊢ (J.plusMap (η ≫ γ)).app x✝ = (J.plusMap η ≫ J.plusMap γ).app x✝

Tactic:
refine colimit.hom_ext (fun S => ?_)

Result:
case w.h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
x✝ : Cᵒᵖ
S : (J.Cover (unop x✝))ᵒᵖ
⊢ colimit.ι (J.diagram P (unop x✝)) S ≫ (J.plusMap (η ≫ γ)).app x✝ =
    colimit.ι (J.diagram P (unop x✝)) S ≫ (J.plusMap η ≫ J.plusMap γ).app x✝

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
⊢ J.plusMap (η ≫ γ) = J.plusMap η ≫ J.plusMap γ

Tactic:
ext : 2

Result:
case w.h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
x✝ : Cᵒᵖ
⊢ (J.plusMap (η ≫ γ)).app x✝ = (J.plusMap η ≫ J.plusMap γ).app x✝
-- Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
theorem intValuation.le_max_iff_min_le {a b c : ℕ} :
    Multiplicative.ofAdd (-c : ℤ) ≤
      max (Multiplicative.ofAdd (-a : ℤ)) (Multiplicative.ofAdd (-b : ℤ)) ↔
      min a b ≤ c

Proof state:
a b c : ℕ
⊢ ofAdd (-↑c) ≤ ofAdd (-↑a) ⊔ ofAdd (-↑b) ↔ a ⊓ b ≤ c

Tactic:
rw [le_max_iff, ofAdd_le, ofAdd_le, neg_le_neg_iff, neg_le_neg_iff, Int.ofNat_le, Int.ofNat_le, ←
  min_le_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem Const.getThenInsertIfNew?_snd_eq [BEq α] [Hashable α] {m : Raw α (fun _ => β)} (h : m.WF)
    {a : α} {b : β} : (Raw.Const.getThenInsertIfNew? m a b).2 =
      (Raw₀.Const.getThenInsertIfNew? ⟨m, h.size_buckets_pos⟩ a b).2.1

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw α fun x => β
h : m.WF
a : α
b : β
⊢ (Raw.Const.getThenInsertIfNew? m a b).snd = (Raw₀.Const.getThenInsertIfNew? ⟨m, ⋯⟩ a b).snd.val

Tactic:
simp [Raw.Const.getThenInsertIfNew?, h.size_buckets_pos]

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem Bounded.dual_iff {t : Ordnode α} {o₁ o₂} :
    Bounded t o₁ o₂ ↔ @Bounded αᵒᵈ _ (.dual t) o₂ o₁ :=
  ⟨Bounded.dual, fun h => by
    have := Bounded.dual h; rwa [dual_dual, OrderDual.Preorder.dual_dual] at this⟩

Proof state:
α : Type u_1
inst✝ : Preorder α
t : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : t.dual.Bounded o₂ o₁
this : t.dual.dual.Bounded o₁ o₂
⊢ t.Bounded o₁ o₂

Tactic:
rwa [dual_dual, OrderDual.Preorder.dual_dual] at this

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
t : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : t.dual.Bounded o₂ o₁
⊢ t.Bounded o₁ o₂

Tactic:
have := Bounded.dual h

Result:
α : Type u_1
inst✝ : Preorder α
t : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : t.dual.Bounded o₂ o₁
this : t.dual.dual.Bounded o₁ o₂
⊢ t.Bounded o₁ o₂
-- Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean
theorem _root_.fourierIntegral_gaussian_innerProductSpace (hb : 0 < b.re) (w : V) :
    𝓕 (fun v ↦ cexp (- b * ‖v‖^2)) w =
      (π / b) ^ (Module.finrank ℝ V / 2 : ℂ) * cexp (-π ^ 2 * ‖w‖^2 / b)

Proof state:
b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
hb : 0 < b.re
w : V
⊢ 𝓕 (fun v => cexp (-b * ↑‖v‖ ^ 2)) w = (↑π / b) ^ (↑(Module.finrank ℝ V) / 2) * cexp (-↑π ^ 2 * ↑‖w‖ ^ 2 / b)

Tactic:
simpa using fourierIntegral_gaussian_innerProductSpace' hb 0 w

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
theorem fderivWithin_const_sub (hxs : UniqueDiffWithinAt 𝕜 s x) (c : F) :
    fderivWithin 𝕜 (fun y => c - f y) s x = -fderivWithin 𝕜 f s x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
hxs : UniqueDiffWithinAt 𝕜 s x
c : F
⊢ fderivWithin 𝕜 (fun y => c - f y) s x = -fderivWithin 𝕜 f s x

Tactic:
simp only [sub_eq_add_neg, fderivWithin_const_add, fderivWithin_neg, hxs]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Bounded.lean
@[to_additive]
lemma NormedCommGroup.cauchySeq_iff [Nonempty α] [SemilatticeSup α] {u : α → E} :
    CauchySeq u ↔ ∀ ε > 0, ∃ N, ∀ m, N ≤ m → ∀ n, N ≤ n → ‖u m / u n‖ < ε

Proof state:
α : Type u_1
E : Type u_2
inst✝² : SeminormedGroup E
inst✝¹ : Nonempty α
inst✝ : SemilatticeSup α
u : α → E
⊢ CauchySeq u ↔ ∀ ε > 0, ∃ N, ∀ (m : α), N ≤ m → ∀ (n : α), N ≤ n → ‖u m / u n‖ < ε

Tactic:
simp [Metric.cauchySeq_iff, dist_eq_norm_div]

Result:
no goals