harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Entails.lean
theorem Incompatible.symm {α : Type u} {σ1 : Type v} {σ2 : Type w} [Entails α σ1]
    [Entails α σ2] (f1 : σ1) (f2 : σ2) :
    Incompatible α f1 f2 ↔ Incompatible α f2 f1

Proof state:
case mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : Entails α σ1
inst✝ : Entails α σ2
f1 : σ1
f2 : σ2
h : Incompatible α f2 f1
a : α → Bool
⊢ ¬(a ⊨ f1) ∨ ¬(a ⊨ f2)

Tactic:
exact Or.symm <| h a

Result:
no goals

Proof state:
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : Entails α σ1
inst✝ : Entails α σ2
f1 : σ1
f2 : σ2
⊢ Incompatible α f1 f2 ↔ Incompatible α f2 f1

Tactic:
constructor

Result:
case mp
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : Entails α σ1
inst✝ : Entails α σ2
f1 : σ1
f2 : σ2
⊢ Incompatible α f1 f2 → Incompatible α f2 f1

case mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : Entails α σ1
inst✝ : Entails α σ2
f1 : σ1
f2 : σ2
⊢ Incompatible α f2 f1 → Incompatible α f1 f2

Proof state:
case mp
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : Entails α σ1
inst✝ : Entails α σ2
f1 : σ1
f2 : σ2
⊢ Incompatible α f1 f2 → Incompatible α f2 f1

Tactic:
intro h a

Result:
case mp
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : Entails α σ1
inst✝ : Entails α σ2
f1 : σ1
f2 : σ2
h : Incompatible α f1 f2
a : α → Bool
⊢ ¬(a ⊨ f2) ∨ ¬(a ⊨ f1)

Proof state:
case mp
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : Entails α σ1
inst✝ : Entails α σ2
f1 : σ1
f2 : σ2
h : Incompatible α f1 f2
a : α → Bool
⊢ ¬(a ⊨ f2) ∨ ¬(a ⊨ f1)

Tactic:
exact Or.symm <| h a

Result:
no goals

Proof state:
case mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : Entails α σ1
inst✝ : Entails α σ2
f1 : σ1
f2 : σ2
⊢ Incompatible α f2 f1 → Incompatible α f1 f2

Tactic:
intro h a

Result:
case mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : Entails α σ1
inst✝ : Entails α σ2
f1 : σ1
f2 : σ2
h : Incompatible α f2 f1
a : α → Bool
⊢ ¬(a ⊨ f1) ∨ ¬(a ⊨ f2)
-- Mathlib/Algebra/Homology/DerivedCategory/Ext/Basic.lean
@[simp]
lemma comp_zero (α : Ext X Y n) (Z : C) (m : ℕ) (p : ℕ) (h : n + m = p) :
    α.comp (0 : Ext Y Z m) h = 0

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
n : ℕ
α : Ext X Y n
Z : C
m p : ℕ
h : n + m = p
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ α.comp 0 h = 0

Tactic:
ext

Result:
case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
n : ℕ
α : Ext X Y n
Z : C
m p : ℕ
h : n + m = p
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ (α.comp 0 h).hom = hom 0

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
n : ℕ
α : Ext X Y n
Z : C
m p : ℕ
h : n + m = p
⊢ α.comp 0 h = 0

Tactic:
letI := HasDerivedCategory.standard C

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
n : ℕ
α : Ext X Y n
Z : C
m p : ℕ
h : n + m = p
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ α.comp 0 h = 0

Proof state:
case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
n : ℕ
α : Ext X Y n
Z : C
m p : ℕ
h : n + m = p
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ (α.comp 0 h).hom = hom 0

Tactic:
simp [this, zero_hom']

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem arg_neg_one : arg (-1) = π

Proof state:
⊢ (-1).arg = π

Tactic:
simp [arg, le_refl, not_le.2 (zero_lt_one' ℝ)]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Diam.lean
lemma exists_dist_eq_diam [Nonempty α] :
    ∃ u v, G.dist u v = G.diam

Proof state:
case h
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
h : ¬G.diam = 0
u v : α
huv : G.edist u v = G.ediam
⊢ G.dist u v = G.diam

Tactic:
rw [diam, dist, congrArg ENat.toNat huv]

Result:
no goals

Proof state:
case neg
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
h : ¬G.diam = 0
⊢ ∃ u v, G.dist u v = G.diam

Tactic:
obtain ⟨u, v, huv⟩ := exists_edist_eq_ediam_of_ne_top <| ediam_ne_top_of_diam_ne_zero h

Result:
case neg.intro.intro
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
h : ¬G.diam = 0
u v : α
huv : G.edist u v = G.ediam
⊢ ∃ u v, G.dist u v = G.diam

Proof state:
case neg.intro.intro
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
h : ¬G.diam = 0
u v : α
huv : G.edist u v = G.ediam
⊢ ∃ u v, G.dist u v = G.diam

Tactic:
use u, v

Result:
case h
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
h : ¬G.diam = 0
u v : α
huv : G.edist u v = G.ediam
⊢ G.dist u v = G.diam

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
⊢ ∃ u v, G.dist u v = G.diam

Tactic:
by_cases h : G.diam = 0

Result:
case pos
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
h : G.diam = 0
⊢ ∃ u v, G.dist u v = G.diam

case neg
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
h : ¬G.diam = 0
⊢ ∃ u v, G.dist u v = G.diam

Proof state:
case pos
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
h : G.diam = 0
⊢ ∃ u v, G.dist u v = G.diam

Tactic:
simp [h]

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
theorem nontrivial_dual_iff :
    Nontrivial (Dual K V) ↔ Nontrivial V

Proof state:
K : Type uK
V : Type uV
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Projective K V
⊢ Nontrivial (Dual K V) ↔ Nontrivial V

Tactic:
rw [← not_iff_not, not_nontrivial_iff_subsingleton, not_nontrivial_iff_subsingleton,
  subsingleton_dual_iff]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Div.lean
lemma leadingCoeff_divByMonic_X_sub_C (p : R[X]) (hp : degree p ≠ 0) (a : R) :
    leadingCoeff (p /ₘ (X - C a)) = leadingCoeff p

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.degree ≠ 0
a : R
⊢ (p /ₘ (X - C a)).leadingCoeff = p.leadingCoeff

Tactic:
nontriviality

Result:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : R[X]
hp : p.degree ≠ 0
a : R
inst✝ : Nontrivial R
⊢ (p /ₘ (X - C a)).leadingCoeff = p.leadingCoeff

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : R[X]
hp : p.degree ≠ 0
a : R
inst✝ : Nontrivial R
⊢ (p /ₘ (X - C a)).leadingCoeff = p.leadingCoeff

Tactic:
rcases hp.lt_or_lt with hd | hd

Result:
case inl
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : R[X]
hp : p.degree ≠ 0
a : R
inst✝ : Nontrivial R
hd : p.degree < 0
⊢ (p /ₘ (X - C a)).leadingCoeff = p.leadingCoeff

case inr
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : R[X]
hp : p.degree ≠ 0
a : R
inst✝ : Nontrivial R
hd : 0 < p.degree
⊢ (p /ₘ (X - C a)).leadingCoeff = p.leadingCoeff

Proof state:
case inr
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : R[X]
hp : p.degree ≠ 0
a : R
inst✝ : Nontrivial R
hd : 0 < p.degree
⊢ (p /ₘ (X - C a)).leadingCoeff = p.leadingCoeff

Tactic:
refine leadingCoeff_divByMonic_of_monic (monic_X_sub_C a) ?_

Result:
case inr
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : R[X]
hp : p.degree ≠ 0
a : R
inst✝ : Nontrivial R
hd : 0 < p.degree
⊢ (X - C a).degree ≤ p.degree

Proof state:
case inl
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : R[X]
hp : p.degree ≠ 0
a : R
inst✝ : Nontrivial R
hd : p.degree < 0
⊢ (p /ₘ (X - C a)).leadingCoeff = p.leadingCoeff

Tactic:
rw [degree_eq_bot.mp <| Nat.WithBot.lt_zero_iff.mp hd, zero_divByMonic]

Result:
no goals

Proof state:
case inr
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : R[X]
hp : p.degree ≠ 0
a : R
inst✝ : Nontrivial R
hd : 0 < p.degree
⊢ (X - C a).degree ≤ p.degree

Tactic:
rwa [degree_X_sub_C, Nat.WithBot.one_le_iff_zero_lt]

Result:
no goals
-- Mathlib/RingTheory/LinearDisjoint.lean
theorem finrank_sup_of_free [Module.Free R A] [Module.Free R B] :
    Module.finrank R ↥(A ⊔ B) = Module.finrank R A * Module.finrank R B

Proof state:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
inst✝¹ : Module.Free R ↥A
inst✝ : Module.Free R ↥B
⊢ Module.finrank R ↥(A ⊔ B) = Module.finrank R ↥A * Module.finrank R ↥B

Tactic:
simpa only [map_mul] using congr(Cardinal.toNat $(H.rank_sup_of_free))

Result:
no goals
-- Mathlib/Order/Hom/Basic.lean
theorem OrderIso.map_inf [SemilatticeInf α] [SemilatticeInf β] (f : α ≃o β) (x y : α) :
    f (x ⊓ y) = f x ⊓ f y

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeInf α
inst✝ : SemilatticeInf β
f : α ≃o β
x y : α
⊢ f.toOrderEmbedding x ⊓ f.toOrderEmbedding y ≤ f.toOrderEmbedding (x ⊓ y)

Tactic:
apply f.symm.le_iff_le.1

Result:
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeInf α
inst✝ : SemilatticeInf β
f : α ≃o β
x y : α
⊢ f.symm (f.toOrderEmbedding x ⊓ f.toOrderEmbedding y) ≤ f.symm (f.toOrderEmbedding (x ⊓ y))

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeInf α
inst✝ : SemilatticeInf β
f : α ≃o β
x y : α
⊢ f.symm (f.toOrderEmbedding x ⊓ f.toOrderEmbedding y) ≤ f.symm (f.toOrderEmbedding (x ⊓ y))

Tactic:
simpa using f.symm.toOrderEmbedding.map_inf_le (f x) (f y)

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeInf α
inst✝ : SemilatticeInf β
f : α ≃o β
x y : α
⊢ f (x ⊓ y) = f x ⊓ f y

Tactic:
refine (f.toOrderEmbedding.map_inf_le x y).antisymm ?_

Result:
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeInf α
inst✝ : SemilatticeInf β
f : α ≃o β
x y : α
⊢ f.toOrderEmbedding x ⊓ f.toOrderEmbedding y ≤ f.toOrderEmbedding (x ⊓ y)
-- Mathlib/CategoryTheory/Sites/Sieves.lean
lemma ofArrows_le_ofObjects
    {I : Type*} (Y : I → C) {X : C} (f : ∀ i, Y i ⟶ X) :
    Sieve.ofArrows Y f ≤ Sieve.ofObjects Y X

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
Y : I → C
X : C
f : (i : I) → Y i ⟶ X
W : C
g : W ⟶ X
hg : ∃ i a, g = a ≫ f i
⊢ (ofObjects Y X).arrows g

Tactic:
obtain ⟨i, a, rfl⟩ := hg

Result:
case intro.intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
Y : I → C
X : C
f : (i : I) → Y i ⟶ X
W : C
i : I
a : W ⟶ Y i
⊢ (ofObjects Y X).arrows (a ≫ f i)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
Y : I → C
X : C
f : (i : I) → Y i ⟶ X
W : C
g : W ⟶ X
hg : (ofArrows Y f).arrows g
⊢ (ofObjects Y X).arrows g

Tactic:
rw [mem_ofArrows_iff] at hg

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
Y : I → C
X : C
f : (i : I) → Y i ⟶ X
W : C
g : W ⟶ X
hg : ∃ i a, g = a ≫ f i
⊢ (ofObjects Y X).arrows g

Proof state:
case intro.intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
Y : I → C
X : C
f : (i : I) → Y i ⟶ X
W : C
i : I
a : W ⟶ Y i
⊢ (ofObjects Y X).arrows (a ≫ f i)

Tactic:
exact ⟨i, ⟨a⟩⟩

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
Y : I → C
X : C
f : (i : I) → Y i ⟶ X
⊢ ofArrows Y f ≤ ofObjects Y X

Tactic:
intro W g hg

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
Y : I → C
X : C
f : (i : I) → Y i ⟶ X
W : C
g : W ⟶ X
hg : (ofArrows Y f).arrows g
⊢ (ofObjects Y X).arrows g
-- Mathlib/Topology/Order/LeftRightNhds.lean
theorem eventually_abs_sub_lt (a : α) {ε : α} (hε : 0 < ε) : ∀ᶠ x in 𝓝 a, |x - a| < ε :=
  (nhds_eq_iInf_abs_sub a).symm ▸
    mem_iInf_of_mem ε (mem_iInf_of_mem hε <| by simp only [abs_sub_comm, mem_principal_self])

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : OrderTopology α
a ε : α
hε : 0 < ε
⊢ {x | (fun x => |x - a| < ε) x} ∈ 𝓟 {b | |a - b| < ε}

Tactic:
simp only [abs_sub_comm, mem_principal_self]

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem diagonal_mulVec_single [Fintype n] [DecidableEq n] [NonUnitalNonAssocSemiring R] (v : n → R)
    (j : n) (x : R) : diagonal v *ᵥ Pi.single j x = Pi.single j (v j * x)

Proof state:
n : Type u_3
R : Type u_7
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : NonUnitalNonAssocSemiring R
v : n → R
j : n
x : R
⊢ diagonal v *ᵥ Pi.single j x = Pi.single j (v j * x)

Tactic:
ext i

Result:
case h
n : Type u_3
R : Type u_7
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : NonUnitalNonAssocSemiring R
v : n → R
j : n
x : R
i : n
⊢ (diagonal v *ᵥ Pi.single j x) i = Pi.single j (v j * x) i

Proof state:
case h
n : Type u_3
R : Type u_7
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : NonUnitalNonAssocSemiring R
v : n → R
j : n
x : R
i : n
⊢ (diagonal v *ᵥ Pi.single j x) i = Pi.single j (v j * x) i

Tactic:
rw [mulVec_diagonal]

Result:
case h
n : Type u_3
R : Type u_7
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : NonUnitalNonAssocSemiring R
v : n → R
j : n
x : R
i : n
⊢ v i * Pi.single j x i = Pi.single j (v j * x) i

Proof state:
case h
n : Type u_3
R : Type u_7
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : NonUnitalNonAssocSemiring R
v : n → R
j : n
x : R
i : n
⊢ v i * Pi.single j x i = Pi.single j (v j * x) i

Tactic:
exact Pi.apply_single (fun i x => v i * x) (fun i => mul_zero _) j x i

Result:
no goals
-- Mathlib/SetTheory/Surreal/Multiplication.lean
lemma P2_neg_left : P2 x₁ x₂ y ↔ P2 (-x₂) (-x₁) y

Proof state:
x₁ x₂ y : PGame
⊢ x₁ ≈ x₂ → ⟦x₁ * y⟧ = ⟦x₂ * y⟧ ↔ -x₂ ≈ -x₁ → ⟦-x₂ * y⟧ = ⟦-x₁ * y⟧

Tactic:
constructor

Result:
case mp
x₁ x₂ y : PGame
⊢ (x₁ ≈ x₂ → ⟦x₁ * y⟧ = ⟦x₂ * y⟧) → -x₂ ≈ -x₁ → ⟦-x₂ * y⟧ = ⟦-x₁ * y⟧

case mpr
x₁ x₂ y : PGame
⊢ (-x₂ ≈ -x₁ → ⟦-x₂ * y⟧ = ⟦-x₁ * y⟧) → x₁ ≈ x₂ → ⟦x₁ * y⟧ = ⟦x₂ * y⟧

Proof state:
case mp
x₁ x₂ y : PGame
⊢ (x₁ ≈ x₂ → ⟦x₁ * y⟧ = ⟦x₂ * y⟧) → -x₂ ≈ -x₁ → ⟦-x₂ * y⟧ = ⟦-x₁ * y⟧

Tactic:
rw [quot_neg_mul, quot_neg_mul, eq_comm, neg_inj, neg_equiv_neg_iff, PGame.equiv_comm]

Result:
case mp
x₁ x₂ y : PGame
⊢ (x₂ ≈ x₁ → ⟦x₂ * y⟧ = ⟦x₁ * y⟧) → x₂ ≈ x₁ → ⟦x₂ * y⟧ = ⟦x₁ * y⟧

Proof state:
x₁ x₂ y : PGame
⊢ P2 x₁ x₂ y ↔ P2 (-x₂) (-x₁) y

Tactic:
rw [P2, P2]

Result:
x₁ x₂ y : PGame
⊢ x₁ ≈ x₂ → ⟦x₁ * y⟧ = ⟦x₂ * y⟧ ↔ -x₂ ≈ -x₁ → ⟦-x₂ * y⟧ = ⟦-x₁ * y⟧

Proof state:
case mpr
x₁ x₂ y : PGame
⊢ (-x₂ ≈ -x₁ → ⟦-x₂ * y⟧ = ⟦-x₁ * y⟧) → x₁ ≈ x₂ → ⟦x₁ * y⟧ = ⟦x₂ * y⟧

Tactic:
rw [PGame.equiv_comm, neg_equiv_neg_iff, quot_neg_mul, quot_neg_mul, neg_inj, eq_comm]

Result:
case mpr
x₁ x₂ y : PGame
⊢ (x₁ ≈ x₂ → ⟦x₁ * y⟧ = ⟦x₂ * y⟧) → x₁ ≈ x₂ → ⟦x₁ * y⟧ = ⟦x₂ * y⟧
-- Mathlib/Data/Real/Hyperreal.lean
theorem st_inv (x : ℝ*) : st x⁻¹ = (st x)⁻¹

Proof state:
x : ℝ*
⊢ x⁻¹.st = x.st⁻¹

Tactic:
by_cases h0 : x = 0

Result:
case pos
x : ℝ*
h0 : x = 0
⊢ x⁻¹.st = x.st⁻¹

case neg
x : ℝ*
h0 : ¬x = 0
⊢ x⁻¹.st = x.st⁻¹

Proof state:
case neg
x : ℝ*
h0 : ¬x = 0
⊢ x⁻¹.st = x.st⁻¹

Tactic:
by_cases h1 : Infinitesimal x

Result:
case pos
x : ℝ*
h0 : ¬x = 0
h1 : x.Infinitesimal
⊢ x⁻¹.st = x.st⁻¹

case neg
x : ℝ*
h0 : ¬x = 0
h1 : ¬x.Infinitesimal
⊢ x⁻¹.st = x.st⁻¹

Proof state:
case neg
x : ℝ*
h0 : ¬x = 0
h1 : ¬x.Infinitesimal
⊢ x⁻¹.st = x.st⁻¹

Tactic:
by_cases h2 : Infinite x

Result:
case pos
x : ℝ*
h0 : ¬x = 0
h1 : ¬x.Infinitesimal
h2 : x.Infinite
⊢ x⁻¹.st = x.st⁻¹

case neg
x : ℝ*
h0 : ¬x = 0
h1 : ¬x.Infinitesimal
h2 : ¬x.Infinite
⊢ x⁻¹.st = x.st⁻¹

Proof state:
case pos
x : ℝ*
h0 : x = 0
⊢ x⁻¹.st = x.st⁻¹

Tactic:
rw [h0, inv_zero, ← coe_zero, st_id_real, inv_zero]

Result:
no goals

Proof state:
case pos
x : ℝ*
h0 : ¬x = 0
h1 : x.Infinitesimal
⊢ x⁻¹.st = x.st⁻¹

Tactic:
rw [((infinitesimal_iff_infinite_inv h0).mp h1).st_eq, h1.st_eq, inv_zero]

Result:
no goals

Proof state:
case neg
x : ℝ*
h0 : ¬x = 0
h1 : ¬x.Infinitesimal
h2 : ¬x.Infinite
⊢ x⁻¹.st = x.st⁻¹

Tactic:
exact ((isSt_st' h2).inv h1).st_eq

Result:
no goals

Proof state:
case pos
x : ℝ*
h0 : ¬x = 0
h1 : ¬x.Infinitesimal
h2 : x.Infinite
⊢ x⁻¹.st = x.st⁻¹

Tactic:
rw [(infinitesimal_inv_of_infinite h2).st_eq, h2.st_eq, inv_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem neg_add_le_right_of_le_add {a b c : Int} (h : a ≤ b + c) : -c + a ≤ b

Proof state:
a b c : Int
h : a ≤ c + b
⊢ -c + a ≤ b

Tactic:
exact Int.neg_add_le_left_of_le_add h

Result:
no goals

Proof state:
a b c : Int
h : a ≤ b + c
⊢ -c + a ≤ b

Tactic:
rw [Int.add_comm] at h

Result:
a b c : Int
h : a ≤ c + b
⊢ -c + a ≤ b
-- Mathlib/CategoryTheory/Limits/FunctorCategory/Shapes/Products.lean
theorem piObjIso_inv_comp_π (f : α → D ⥤ C) (d : D) (s : α) :
    (piObjIso f d).inv ≫ (Pi.π f s).app d = Pi.π (fun s => (f s).obj d) s

Proof state:
C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
α : Type w
inst✝ : HasLimitsOfShape (Discrete α) C
f : α → D ⥤ C
d : D
s : α
⊢ (piObjIso f d).inv ≫ (Pi.π f s).app d = Pi.π (fun s => (f s).obj d) s

Tactic:
simp [piObjIso]

Result:
no goals
-- Mathlib/Data/NNRat/Defs.lean
@[simp] lemma num_pos : 0 < q.num ↔ 0 < q

Proof state:
q : ℚ≥0
⊢ 0 < q.num ↔ 0 < q

Tactic:
simpa [num, -nonpos_iff_eq_zero] using nonpos_iff_eq_zero _ |>.not.symm

Result:
no goals
-- Mathlib/RingTheory/GradedAlgebra/Basic.lean
theorem coe_decompose_mul_of_right_mem_of_le (b_mem : b ∈ 𝒜 i) (h : i ≤ n) :
    (decompose 𝒜 (a * b) n : A) = decompose 𝒜 a (n - i) * b

Proof state:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝¹⁰ : Semiring A
inst✝⁹ : DecidableEq ι
inst✝⁸ : AddCommMonoid ι
inst✝⁷ : PartialOrder ι
inst✝⁶ : CanonicallyOrderedAdd ι
inst✝⁵ : SetLike σ A
inst✝⁴ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝³ : GradedRing 𝒜
a b : A
n i : ι
inst✝² : Sub ι
inst✝¹ : OrderedSub ι
inst✝ : AddLeftReflectLE ι
b_mem : b ∈ 𝒜 i
h : i ≤ n
⊢ ↑(((decompose 𝒜) (a * b)) n) = ↑(((decompose 𝒜) a) (n - i)) * b

Tactic:
lift b to 𝒜 i using b_mem

Result:
case intro
ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝¹⁰ : Semiring A
inst✝⁹ : DecidableEq ι
inst✝⁸ : AddCommMonoid ι
inst✝⁷ : PartialOrder ι
inst✝⁶ : CanonicallyOrderedAdd ι
inst✝⁵ : SetLike σ A
inst✝⁴ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝³ : GradedRing 𝒜
a : A
n i : ι
inst✝² : Sub ι
inst✝¹ : OrderedSub ι
inst✝ : AddLeftReflectLE ι
h : i ≤ n
b : ↥(𝒜 i)
⊢ ↑(((decompose 𝒜) (a * ↑b)) n) = ↑(((decompose 𝒜) a) (n - i)) * ↑b

Proof state:
case intro
ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝¹⁰ : Semiring A
inst✝⁹ : DecidableEq ι
inst✝⁸ : AddCommMonoid ι
inst✝⁷ : PartialOrder ι
inst✝⁶ : CanonicallyOrderedAdd ι
inst✝⁵ : SetLike σ A
inst✝⁴ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝³ : GradedRing 𝒜
a : A
n i : ι
inst✝² : Sub ι
inst✝¹ : OrderedSub ι
inst✝ : AddLeftReflectLE ι
h : i ≤ n
b : ↥(𝒜 i)
⊢ ↑(((decompose 𝒜) (a * ↑b)) n) = ↑(((decompose 𝒜) a) (n - i)) * ↑b

Tactic:
rwa [decompose_mul, decompose_coe, coe_mul_of_apply_of_le]

Result:
no goals
-- Mathlib/Algebra/Polynomial/AlgebraMap.lean
theorem algEquivCMulXAddC_symm_eq {R : Type*} [CommRing R] (a b : R) [Invertible a] :
    (algEquivCMulXAddC a b).symm =  algEquivCMulXAddC (⅟ a) (- ⅟ a * b)

Proof state:
R : Type u_3
inst✝¹ : CommRing R
a b : R
inst✝ : Invertible a
⊢ (algEquivCMulXAddC a b).symm = algEquivCMulXAddC (⅟a) (-⅟a * b)

Tactic:
ext p : 1

Result:
case h
R : Type u_3
inst✝¹ : CommRing R
a b : R
inst✝ : Invertible a
p : R[X]
⊢ (algEquivCMulXAddC a b).symm p = (algEquivCMulXAddC (⅟a) (-⅟a * b)) p

Proof state:
case h.e_a.e_x
R : Type u_3
inst✝¹ : CommRing R
a b : R
inst✝ : Invertible a
p : R[X]
⊢ C ⅟a * (X - C b) = C ⅟a * X + -(C ⅟a * C b)

Tactic:
simp [mul_add, sub_eq_add_neg]

Result:
no goals

Proof state:
case h
R : Type u_3
inst✝¹ : CommRing R
a b : R
inst✝ : Invertible a
p : R[X]
⊢ (aeval (C ⅟a * (X - C b))) p = (aeval (C ⅟a * X + -(C ⅟a * C b))) p

Tactic:
congr

Result:
case h.e_a.e_x
R : Type u_3
inst✝¹ : CommRing R
a b : R
inst✝ : Invertible a
p : R[X]
⊢ C ⅟a * (X - C b) = C ⅟a * X + -(C ⅟a * C b)

Proof state:
case h
R : Type u_3
inst✝¹ : CommRing R
a b : R
inst✝ : Invertible a
p : R[X]
⊢ (algEquivCMulXAddC a b).symm p = (algEquivCMulXAddC (⅟a) (-⅟a * b)) p

Tactic:
simp only [algEquivCMulXAddC_symm_apply, neg_mul, algEquivCMulXAddC_apply, map_neg, map_mul]

Result:
case h
R : Type u_3
inst✝¹ : CommRing R
a b : R
inst✝ : Invertible a
p : R[X]
⊢ (aeval (C ⅟a * (X - C b))) p = (aeval (C ⅟a * X + -(C ⅟a * C b))) p
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem back?_attachWith {P : α → Prop} {xs : Vector α n}
    {H : ∀ (a : α), a ∈ xs → P a} :
    (xs.attachWith P H).back? = xs.back?.pbind (fun a h => some ⟨a, H _ (mem_of_back? h)⟩)

Proof state:
case mk
α : Type u_1
n : Nat
P : α → Prop
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
H : ∀ (a : α), a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } → P a
⊢ ({ toArray := toArray✝, size_toArray := size_toArray✝ }.attachWith P H).back? =
    { toArray := toArray✝, size_toArray := size_toArray✝ }.back?.pbind fun a h => some ⟨a, ⋯⟩

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
P : α → Prop
xs : Vector α n
H : ∀ (a : α), a ∈ xs → P a
⊢ (xs.attachWith P H).back? = xs.back?.pbind fun a h => some ⟨a, ⋯⟩

Tactic:
cases xs

Result:
case mk
α : Type u_1
n : Nat
P : α → Prop
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
H : ∀ (a : α), a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } → P a
⊢ ({ toArray := toArray✝, size_toArray := size_toArray✝ }.attachWith P H).back? =
    { toArray := toArray✝, size_toArray := size_toArray✝ }.back?.pbind fun a h => some ⟨a, ⋯⟩
-- Mathlib/Data/Set/SMulAntidiagonal.lean
theorem fst_eq_fst_iff_snd_eq_snd :
    (x : G × P).1 = (y : G × P).1 ↔ (x : G × P).2 = (y : G × P).2 :=
  ⟨fun h =>
    IsCancelSMul.left_cancel _ _ _
      (y.2.2.2.trans <| by
          rw [← h]
          exact x.2.2.2.symm).symm,
    fun h =>
    IsCancelSMul.right_cancel _ _ _
      (y.2.2.2.trans <| by
          rw [← h]
          exact x.2.2.2.symm).symm⟩

Proof state:
G : Type u_1
P : Type u_2
s : Set G
t : Set P
a : P
inst✝¹ : SMul G P
inst✝ : IsCancelSMul G P
x y : ↑(s.smulAntidiagonal t a)
h : (↑x).2 = (↑y).2
⊢ a = (↑x).1 • (↑y).2

Tactic:
rw [← h]

Result:
G : Type u_1
P : Type u_2
s : Set G
t : Set P
a : P
inst✝¹ : SMul G P
inst✝ : IsCancelSMul G P
x y : ↑(s.smulAntidiagonal t a)
h : (↑x).2 = (↑y).2
⊢ a = (↑x).1 • (↑x).2

Proof state:
G : Type u_1
P : Type u_2
s : Set G
t : Set P
a : P
inst✝¹ : SMul G P
inst✝ : IsCancelSMul G P
x y : ↑(s.smulAntidiagonal t a)
h : (↑x).1 = (↑y).1
⊢ a = (↑x).1 • (↑x).2

Tactic:
exact x.2.2.2.symm

Result:
no goals

Proof state:
G : Type u_1
P : Type u_2
s : Set G
t : Set P
a : P
inst✝¹ : SMul G P
inst✝ : IsCancelSMul G P
x y : ↑(s.smulAntidiagonal t a)
h : (↑x).2 = (↑y).2
⊢ a = (↑x).1 • (↑x).2

Tactic:
exact x.2.2.2.symm

Result:
no goals

Proof state:
G : Type u_1
P : Type u_2
s : Set G
t : Set P
a : P
inst✝¹ : SMul G P
inst✝ : IsCancelSMul G P
x y : ↑(s.smulAntidiagonal t a)
h : (↑x).1 = (↑y).1
⊢ a = (↑y).1 • (↑x).2

Tactic:
rw [← h]

Result:
G : Type u_1
P : Type u_2
s : Set G
t : Set P
a : P
inst✝¹ : SMul G P
inst✝ : IsCancelSMul G P
x y : ↑(s.smulAntidiagonal t a)
h : (↑x).1 = (↑y).1
⊢ a = (↑x).1 • (↑x).2
-- Mathlib/Order/LiminfLimsup.lean
lemma limsup_sup_filter {g} : limsup u (f ⊔ g) = limsup u f ⊔ limsup u g

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteDistribLattice α
f : Filter β
u : β → α
g : Filter β
⊢ limsup u (f ⊔ g) = limsup u f ⊔ limsup u g

Tactic:
refine le_antisymm ?_
  (sup_le (limsup_le_limsup_of_le le_sup_left) (limsup_le_limsup_of_le le_sup_right))

Result:
α : Type u_1
β : Type u_2
inst✝ : CompleteDistribLattice α
f : Filter β
u : β → α
g : Filter β
⊢ limsup u (f ⊔ g) ≤ limsup u f ⊔ limsup u g

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteDistribLattice α
f : Filter β
u : β → α
g : Filter β
a : α
ha : ∀ᶠ (n : β) in f, u n ≤ a
b : α
hb : ∀ᶠ (n : β) in g, u n ≤ b
⊢ sInf {a | ∀ᶠ (n : β) in f ⊔ g, u n ≤ a} ≤ a ⊔ b

Tactic:
exact sInf_le ⟨ha.mono fun _ h ↦ h.trans le_sup_left, hb.mono fun _ h ↦ h.trans le_sup_right⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteDistribLattice α
f : Filter β
u : β → α
g : Filter β
⊢ limsup u (f ⊔ g) ≤ limsup u f ⊔ limsup u g

Tactic:
simp_rw [limsup_eq, sInf_sup_eq, sup_sInf_eq, mem_setOf_eq, le_iInf₂_iff]

Result:
α : Type u_1
β : Type u_2
inst✝ : CompleteDistribLattice α
f : Filter β
u : β → α
g : Filter β
⊢ ∀ (i : α),
    (∀ᶠ (n : β) in f, u n ≤ i) →
      ∀ (i_1 : α), (∀ᶠ (n : β) in g, u n ≤ i_1) → sInf {a | ∀ᶠ (n : β) in f ⊔ g, u n ≤ a} ≤ i ⊔ i_1

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteDistribLattice α
f : Filter β
u : β → α
g : Filter β
⊢ ∀ (i : α),
    (∀ᶠ (n : β) in f, u n ≤ i) →
      ∀ (i_1 : α), (∀ᶠ (n : β) in g, u n ≤ i_1) → sInf {a | ∀ᶠ (n : β) in f ⊔ g, u n ≤ a} ≤ i ⊔ i_1

Tactic:
intro a ha b hb

Result:
α : Type u_1
β : Type u_2
inst✝ : CompleteDistribLattice α
f : Filter β
u : β → α
g : Filter β
a : α
ha : ∀ᶠ (n : β) in f, u n ≤ a
b : α
hb : ∀ᶠ (n : β) in g, u n ≤ b
⊢ sInf {a | ∀ᶠ (n : β) in f ⊔ g, u n ≤ a} ≤ a ⊔ b