harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/Group/Abs.lean
@[to_additive] lemma mabs_pow (n : ℕ) (a : α) : |a ^ n|ₘ = |a|ₘ ^ n

Proof state:
case inr
α : Type u_1
inst✝ : LinearOrderedCommGroup α
n : ℕ
a : α
ha : 1 ≤ a
⊢ mabs (a ^ n) = mabs a ^ n

Tactic:
rw [mabs_of_one_le ha, mabs_of_one_le (one_le_pow_of_one_le' ha n)]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedCommGroup α
n : ℕ
a : α
⊢ mabs (a ^ n) = mabs a ^ n

Tactic:
obtain ha | ha := le_total a 1

Result:
case inl
α : Type u_1
inst✝ : LinearOrderedCommGroup α
n : ℕ
a : α
ha : a ≤ 1
⊢ mabs (a ^ n) = mabs a ^ n

case inr
α : Type u_1
inst✝ : LinearOrderedCommGroup α
n : ℕ
a : α
ha : 1 ≤ a
⊢ mabs (a ^ n) = mabs a ^ n

Proof state:
case inl
α : Type u_1
inst✝ : LinearOrderedCommGroup α
n : ℕ
a : α
ha : a ≤ 1
⊢ 1 ≤ a⁻¹ ^ n

Tactic:
exact one_le_pow_of_one_le' (one_le_inv'.2 ha) n

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝ : LinearOrderedCommGroup α
n : ℕ
a : α
ha : a ≤ 1
⊢ mabs (a ^ n) = mabs a ^ n

Tactic:
rw [mabs_of_le_one ha, ← mabs_inv, ← inv_pow, mabs_of_one_le]

Result:
case inl
α : Type u_1
inst✝ : LinearOrderedCommGroup α
n : ℕ
a : α
ha : a ≤ 1
⊢ 1 ≤ a⁻¹ ^ n
-- Mathlib/Data/List/Intervals.lean
theorem chain'_succ (n m : ℕ) : Chain' (fun a b => b = succ a) (Ico n m)

Proof state:
case neg
n m : ℕ
h : ¬n < m
⊢ Chain' (fun a b => b = a.succ) (Ico n m)

Tactic:
rw [eq_nil_of_le (le_of_not_gt h)]

Result:
case neg
n m : ℕ
h : ¬n < m
⊢ Chain' (fun a b => b = a.succ) []

Proof state:
n m : ℕ
⊢ Chain' (fun a b => b = a.succ) (Ico n m)

Tactic:
by_cases h : n < m

Result:
case pos
n m : ℕ
h : n < m
⊢ Chain' (fun a b => b = a.succ) (Ico n m)

case neg
n m : ℕ
h : ¬n < m
⊢ Chain' (fun a b => b = a.succ) (Ico n m)

Proof state:
case pos
n m : ℕ
h : n < m
⊢ Chain' (fun a b => b = a.succ) (Ico n m)

Tactic:
rw [eq_cons h]

Result:
case pos
n m : ℕ
h : n < m
⊢ Chain' (fun a b => b = a.succ) (n :: Ico (n + 1) m)

Proof state:
case neg
n m : ℕ
h : ¬n < m
⊢ Chain' (fun a b => b = a.succ) []

Tactic:
trivial

Result:
no goals

Proof state:
case pos
n m : ℕ
h : n < m
⊢ Chain' (fun a b => b = a.succ) (n :: Ico (n + 1) m)

Tactic:
exact chain_succ_range' _ _ 1

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Basic.lean
theorem coeff_X_pow [DecidableEq σ] (i : σ) (m) (k : ℕ) :
    coeff m (X i ^ k : MvPolynomial σ R) = if Finsupp.single i k = m then 1 else 0

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i : σ
m : σ →₀ ℕ
k : ℕ
⊢ coeff m (X i ^ k) = if Finsupp.single i k = m then 1 else 0

Tactic:
have := coeff_monomial m (Finsupp.single i k) (1 : R)

Result:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i : σ
m : σ →₀ ℕ
k : ℕ
this : coeff m ((monomial (Finsupp.single i k)) 1) = if Finsupp.single i k = m then 1 else 0
⊢ coeff m (X i ^ k) = if Finsupp.single i k = m then 1 else 0

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i : σ
m : σ →₀ ℕ
k : ℕ
this : coeff m ((Finsupp.single i k).prod fun n e => X n ^ e) = if Finsupp.single i k = m then 1 else 0
⊢ X i ^ 0 = 1

Tactic:
exact pow_zero _

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i : σ
m : σ →₀ ℕ
k : ℕ
this : coeff m ((monomial (Finsupp.single i k)) 1) = if Finsupp.single i k = m then 1 else 0
⊢ coeff m (X i ^ k) = if Finsupp.single i k = m then 1 else 0

Tactic:
rwa [@monomial_eq _ _ (1 : R) (Finsupp.single i k) _, C_1, one_mul, Finsupp.prod_single_index]
  at this

Result:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i : σ
m : σ →₀ ℕ
k : ℕ
this : coeff m ((Finsupp.single i k).prod fun n e => X n ^ e) = if Finsupp.single i k = m then 1 else 0
⊢ X i ^ 0 = 1
-- Mathlib/RingTheory/RingHom/StandardSmooth.lean
lemma IsStandardSmoothOfRelativeDimension.equiv (e : R ≃+* S) :
    IsStandardSmoothOfRelativeDimension.{t, w} 0 (e : R →+* S)

Proof state:
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
e : R ≃+* S
algInst✝ : Algebra R S := e.toRingHom.toAlgebra
⊢ IsStandardSmoothOfRelativeDimension 0 ↑e

Tactic:
exact Algebra.IsStandardSmoothOfRelativeDimension.of_algebraMap_bijective e.bijective

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
e : R ≃+* S
⊢ IsStandardSmoothOfRelativeDimension 0 ↑e

Tactic:
algebraize [e.toRingHom]

Result:
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
e : R ≃+* S
algInst✝ : Algebra R S := e.toRingHom.toAlgebra
⊢ IsStandardSmoothOfRelativeDimension 0 ↑e
-- Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean
lemma det_one_add_X_smul (M : Matrix n n R) :
    det (1 + (X : R[X]) • M.map C) =
      (1 : R[X]) + trace M • X + (det (1 + (X : R[X]) • M.map C)).divX.divX * X ^ 2

Proof state:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ (1 + X • M.map ⇑C).det = (1 + X • M.map ⇑C).det.divX * X + C 1

Tactic:
convert (divX_mul_X_add _).symm

Result:
case h.e'_3.h.e'_6.h.e'_6
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ 1 = (1 + X • M.map ⇑C).det.coeff 0

Proof state:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ (1 + X • M.map ⇑C).det = 1 + M.trace • X + (1 + X • M.map ⇑C).det.divX.divX * X ^ 2

Tactic:
rw [Algebra.smul_def (trace M), ← C_eq_algebraMap, pow_two, ← mul_assoc, add_assoc,
  ← add_mul, ← coeff_det_one_add_X_smul_one, ← coeff_divX, add_comm (C _), divX_mul_X_add,
  add_comm (1 : R[X]), ← C.map_one]

Result:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ (1 + X • M.map ⇑C).det = (1 + X • M.map ⇑C).det.divX * X + C 1

Proof state:
case h.e'_3.h.e'_6.h.e'_6
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ 1 = (1 + X • M.map ⇑C).det.coeff 0

Tactic:
rw [coeff_zero_eq_eval_zero, eval_det_add_X_smul, det_one, eval_one]

Result:
no goals
-- Mathlib/Analysis/Convex/Side.lean
theorem isPreconnected_setOf_wOppSide (s : AffineSubspace ℝ P) (x : P) :
    IsPreconnected { y | s.WOppSide x y }

Proof state:
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
⊢ IsPreconnected {y | s.WOppSide x y}

Tactic:
rcases Set.eq_empty_or_nonempty (s : Set P) with (h | h)

Result:
case inl
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : ↑s = ∅
⊢ IsPreconnected {y | s.WOppSide x y}

case inr
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : (↑s).Nonempty
⊢ IsPreconnected {y | s.WOppSide x y}

Proof state:
case inr
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : (↑s).Nonempty
⊢ IsPreconnected {y | s.WOppSide x y}

Tactic:
exact (isConnected_setOf_wOppSide x h).isPreconnected

Result:
no goals

Proof state:
case inl
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : s = ⊥
⊢ IsPreconnected {y | False}

Tactic:
exact isPreconnected_empty

Result:
no goals

Proof state:
case inl
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : s = ⊥
⊢ IsPreconnected {y | s.WOppSide x y}

Tactic:
simp only [h, not_wOppSide_bot]

Result:
case inl
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : s = ⊥
⊢ IsPreconnected {y | False}

Proof state:
case inl
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : ↑s = ∅
⊢ IsPreconnected {y | s.WOppSide x y}

Tactic:
rw [coe_eq_bot_iff] at h

Result:
case inl
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : s = ⊥
⊢ IsPreconnected {y | s.WOppSide x y}
-- Mathlib/Data/List/Cycle.lean
theorem next_reverse_eq_prev (l : List α) (h : Nodup l) (x : α) (hx : x ∈ l) :
    next l.reverse x (mem_reverse.mpr hx) = prev l x hx

Proof state:
case h.e'_3.h.e'_3
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
x : α
hx : x ∈ l
⊢ l = l.reverse.reverse

Tactic:
exact (reverse_reverse l).symm

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
x : α
hx : x ∈ l
⊢ l.reverse.next x ⋯ = l.prev x hx

Tactic:
convert (prev_reverse_eq_next l.reverse (nodup_reverse.mpr h) x (mem_reverse.mpr hx)).symm

Result:
case h.e'_3.h.e'_3
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
x : α
hx : x ∈ l
⊢ l = l.reverse.reverse
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
lemma cfcₙ_apply_of_not_continuousOn {f : R → R} (a : A) (hf : ¬ ContinuousOn f (σₙ R a)) :
    cfcₙ f a = 0

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
f : R → R
a : A
hf : ¬ContinuousOn f (σₙ R a)
⊢ cfcₙ f a = 0

Tactic:
rw [cfcₙ_def, dif_neg (not_and_of_not_right _ (not_and_of_not_left _ hf))]

Result:
no goals
-- Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.lean
theorem Submodule.span_range_natDegree_eq_adjoin {R A} [CommRing R] [Semiring A] [Algebra R A]
    {x : A} {f : R[X]} (hf : f.Monic) (hfx : aeval x f = 0) :
    span R (Finset.image (x ^ ·) (Finset.range (natDegree f))) =
      Subalgebra.toSubmodule (Algebra.adjoin R {x})

Proof state:
case refine_2
R : Type u_5
A : Type u_6
inst✝² : CommRing R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
f : R[X]
hf : f.Monic
hfx : (aeval x) f = 0
a✝ : Nontrivial A
hf1 : f ≠ 1
r : A
hr : r ∈ Subalgebra.toSubmodule (Algebra.adjoin R {x})
⊢ r ∈ span R ↑(Finset.image (fun x_1 => x ^ x_1) (Finset.range f.natDegree))

Tactic:
rw [Subalgebra.mem_toSubmodule, Algebra.adjoin_singleton_eq_range_aeval] at hr

Result:
case refine_2
R : Type u_5
A : Type u_6
inst✝² : CommRing R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
f : R[X]
hf : f.Monic
hfx : (aeval x) f = 0
a✝ : Nontrivial A
hf1 : f ≠ 1
r : A
hr : r ∈ (aeval x).range
⊢ r ∈ span R ↑(Finset.image (fun x_1 => x ^ x_1) (Finset.range f.natDegree))

Proof state:
case refine_2.intro
R : Type u_5
A : Type u_6
inst✝² : CommRing R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
f : R[X]
hf : f.Monic
hfx : (aeval x) f = 0
a✝ : Nontrivial A
hf1 : f ≠ 1
p : R[X]
hr : (aeval x) p ∈ (aeval x).range
k : ℕ
hkq : k ∈ (p %ₘ f).support
⊢ eval₂ (algebraMap R A) x (C ((p %ₘ f).coeff k) * X ^ k) ∈
    span R ↑(Finset.image (fun x_1 => x ^ x_1) (Finset.range f.natDegree))

Tactic:
rw [C_mul_X_pow_eq_monomial, eval₂_monomial, ← Algebra.smul_def]

Result:
case refine_2.intro
R : Type u_5
A : Type u_6
inst✝² : CommRing R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
f : R[X]
hf : f.Monic
hfx : (aeval x) f = 0
a✝ : Nontrivial A
hf1 : f ≠ 1
p : R[X]
hr : (aeval x) p ∈ (aeval x).range
k : ℕ
hkq : k ∈ (p %ₘ f).support
⊢ (p %ₘ f).coeff k • x ^ k ∈ span R ↑(Finset.image (fun x_1 => x ^ x_1) (Finset.range f.natDegree))
-- Mathlib/Combinatorics/SimpleGraph/Triangle/Tripartite.lean
lemma cliqueFinset_eq_image [NoAccidental t] : (graph t).cliqueFinset 3 = t.image toTriangle :=
  coe_injective <| by push_cast; exact cliqueSet_eq_image _

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝⁶ : DecidableEq α
inst✝⁵ : DecidableEq β
inst✝⁴ : DecidableEq γ
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype γ
inst✝ : NoAccidental t
⊢ ↑((graph t).cliqueFinset 3) = ↑(image (⇑toTriangle) t)

Tactic:
push_cast

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝⁶ : DecidableEq α
inst✝⁵ : DecidableEq β
inst✝⁴ : DecidableEq γ
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype γ
inst✝ : NoAccidental t
⊢ (graph t).cliqueSet 3 = ⇑toTriangle '' ↑t

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝⁶ : DecidableEq α
inst✝⁵ : DecidableEq β
inst✝⁴ : DecidableEq γ
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype γ
inst✝ : NoAccidental t
⊢ (graph t).cliqueSet 3 = ⇑toTriangle '' ↑t

Tactic:
exact cliqueSet_eq_image _

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Addition.lean
theorem min_order_le_order_add {Γ} [Zero Γ] [LinearOrder Γ] {x y : HahnSeries Γ R}
    (hxy : x + y ≠ 0) : min x.order y.order ≤ (x + y).order

Proof state:
case pos
R : Type u_3
inst✝² : AddMonoid R
Γ : Type u_8
inst✝¹ : Zero Γ
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hxy : x + y ≠ 0
hx : x = 0
⊢ x.order ⊓ y.order ≤ (x + y).order

Tactic:
simp [hx]

Result:
no goals

Proof state:
case pos
R : Type u_3
inst✝² : AddMonoid R
Γ : Type u_8
inst✝¹ : Zero Γ
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hxy : x + y ≠ 0
hx : ¬x = 0
hy : y = 0
⊢ x.order ⊓ y.order ≤ (x + y).order

Tactic:
simp [hy]

Result:
no goals

Proof state:
case neg
R : Type u_3
inst✝² : AddMonoid R
Γ : Type u_8
inst✝¹ : Zero Γ
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hxy : x + y ≠ 0
hx : ¬x = 0
hy : ¬y = 0
⊢ ⋯.min ⋯ ⊓ ⋯.min ⋯ ≤ ⋯.min ⋯

Tactic:
exact HahnSeries.min_le_min_add hx hy hxy

Result:
no goals

Proof state:
case neg
R : Type u_3
inst✝² : AddMonoid R
Γ : Type u_8
inst✝¹ : Zero Γ
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hxy : x + y ≠ 0
hx : ¬x = 0
hy : ¬y = 0
⊢ x.order ⊓ y.order ≤ (x + y).order

Tactic:
rw [order_of_ne hx, order_of_ne hy, order_of_ne hxy]

Result:
case neg
R : Type u_3
inst✝² : AddMonoid R
Γ : Type u_8
inst✝¹ : Zero Γ
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hxy : x + y ≠ 0
hx : ¬x = 0
hy : ¬y = 0
⊢ ⋯.min ⋯ ⊓ ⋯.min ⋯ ≤ ⋯.min ⋯

Proof state:
case neg
R : Type u_3
inst✝² : AddMonoid R
Γ : Type u_8
inst✝¹ : Zero Γ
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hxy : x + y ≠ 0
hx : ¬x = 0
⊢ x.order ⊓ y.order ≤ (x + y).order

Tactic:
by_cases hy : y = 0

Result:
case pos
R : Type u_3
inst✝² : AddMonoid R
Γ : Type u_8
inst✝¹ : Zero Γ
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hxy : x + y ≠ 0
hx : ¬x = 0
hy : y = 0
⊢ x.order ⊓ y.order ≤ (x + y).order

case neg
R : Type u_3
inst✝² : AddMonoid R
Γ : Type u_8
inst✝¹ : Zero Γ
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hxy : x + y ≠ 0
hx : ¬x = 0
hy : ¬y = 0
⊢ x.order ⊓ y.order ≤ (x + y).order

Proof state:
R : Type u_3
inst✝² : AddMonoid R
Γ : Type u_8
inst✝¹ : Zero Γ
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hxy : x + y ≠ 0
⊢ x.order ⊓ y.order ≤ (x + y).order

Tactic:
by_cases hx : x = 0

Result:
case pos
R : Type u_3
inst✝² : AddMonoid R
Γ : Type u_8
inst✝¹ : Zero Γ
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hxy : x + y ≠ 0
hx : x = 0
⊢ x.order ⊓ y.order ≤ (x + y).order

case neg
R : Type u_3
inst✝² : AddMonoid R
Γ : Type u_8
inst✝¹ : Zero Γ
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hxy : x + y ≠ 0
hx : ¬x = 0
⊢ x.order ⊓ y.order ≤ (x + y).order
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem getElem_add_add_bool {i : Nat} (i_lt : i < w) (x y : BitVec w) (c : Bool) :
    (x + y + setWidth w (ofBool c))[i] =
      (x[i] ^^ (y[i] ^^ carry i x y c))

Proof state:
w i : Nat
i_lt : i < w
x y : BitVec w
c : Bool
⊢ (x + y + setWidth w (ofBool c))[i] = (x[i] ^^ (y[i] ^^ carry i x y c))

Tactic:
simp only [← getLsbD_eq_getElem]

Result:
w i : Nat
i_lt : i < w
x y : BitVec w
c : Bool
⊢ (x + y + setWidth w (ofBool c)).getLsbD i = (x.getLsbD i ^^ (y.getLsbD i ^^ carry i x y c))

Proof state:
w i : Nat
i_lt : i < w
x y : BitVec w
c : Bool
⊢ (x + y + setWidth w (ofBool c)).getLsbD i = (x.getLsbD i ^^ (y.getLsbD i ^^ carry i x y c))

Tactic:
rw [getLsbD_add_add_bool]

Result:
case i_lt
w i : Nat
i_lt : i < w
x y : BitVec w
c : Bool
⊢ i < w

Proof state:
case i_lt
w i : Nat
i_lt : i < w
x y : BitVec w
c : Bool
⊢ i < w

Tactic:
omega

Result:
no goals
-- Mathlib/Analysis/Meromorphic/Order.lean
/-- The order of a meromorphic function `f` at a `z₀` is infinity iff `f` vanishes locally around
`z₀`. -/
lemma order_eq_top_iff {f : 𝕜 → E} {x : 𝕜} (hf : MeromorphicAt f x) :
    hf.order = ⊤ ↔ ∀ᶠ z in 𝓝[≠] x, f z = 0

Proof state:
case neg.intro.h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
m : ℕ
hm : ↑m = ⋯.order
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝[≠] x, (x_1 - x) ^ Exists.choose hf • f x_1 = 0

Tactic:
filter_upwards [h] with z hfz

Result:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
m : ℕ
hm : ↑m = ⋯.order
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
z : 𝕜
hfz : f z = 0
⊢ (z - x) ^ Exists.choose hf • f z = 0
-- Mathlib/Algebra/Group/Subgroup/ZPowers/Basic.lean
theorem zpowers_inv : zpowers g⁻¹ = zpowers g :=
  eq_of_forall_ge_iff fun _ ↦ by simp only [zpowers_le, inv_mem_iff]

Proof state:
G : Type u_1
inst✝ : Group G
g : G
x✝ : Subgroup G
⊢ zpowers g⁻¹ ≤ x✝ ↔ zpowers g ≤ x✝

Tactic:
simp only [zpowers_le, inv_mem_iff]

Result:
no goals
-- Mathlib/Algebra/Ring/Defs.lean
lemma add_sq (a b : α) : (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2

Proof state:
α : Type u
inst✝ : CommSemiring α
a b : α
⊢ (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2

Tactic:
simp only [sq, add_mul_self_eq]

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
theorem set_eventuallyEq_iff_inf_principal {s t : Set α} {l : Filter α} :
    s =ᶠ[l] t ↔ l ⊓ 𝓟 s = l ⊓ 𝓟 t

Proof state:
α : Type u
s t : Set α
l : Filter α
⊢ s =ᶠ[l] t ↔ l ⊓ 𝓟 s = l ⊓ 𝓟 t

Tactic:
simp only [eventuallyLE_antisymm_iff, le_antisymm_iff, set_eventuallyLE_iff_inf_principal_le]

Result:
no goals
-- Mathlib/Algebra/Module/Defs.lean
theorem neg_smul_neg : -r • -x = r • x

Proof state:
R : Type u_1
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
x : M
⊢ -r • -x = r • x

Tactic:
rw [neg_smul, smul_neg, neg_neg]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ico_union_Ici' (h₁ : c ≤ b) : Ico a b ∪ Ici c = Ici (min a c)

Proof state:
case pos
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ b
x : α
hc : c ≤ x
⊢ a ≤ x ∧ x < b ∨ c ≤ x ↔ a ≤ x ∨ c ≤ x

Tactic:
simp only [hc, or_true]

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ b
x : α
hc : ¬c ≤ x
⊢ a ≤ x ∧ x < b ∨ c ≤ x ↔ a ≤ x ∨ c ≤ x

Tactic:
have hxb : x < b := (lt_of_not_ge hc).trans_le h₁

Result:
case neg
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ b
x : α
hc : ¬c ≤ x
hxb : x < b
⊢ a ≤ x ∧ x < b ∨ c ≤ x ↔ a ≤ x ∨ c ≤ x

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ b
⊢ Ico a b ∪ Ici c = Ici (a ⊓ c)

Tactic:
ext1 x

Result:
case h
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ b
x : α
⊢ x ∈ Ico a b ∪ Ici c ↔ x ∈ Ici (a ⊓ c)

Proof state:
case neg
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ b
x : α
hc : ¬c ≤ x
hxb : x < b
⊢ a ≤ x ∧ x < b ∨ c ≤ x ↔ a ≤ x ∨ c ≤ x

Tactic:
simp only [hxb, and_true]

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ b
x : α
⊢ a ≤ x ∧ x < b ∨ c ≤ x ↔ a ≤ x ∨ c ≤ x

Tactic:
by_cases hc : c ≤ x

Result:
case pos
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ b
x : α
hc : c ≤ x
⊢ a ≤ x ∧ x < b ∨ c ≤ x ↔ a ≤ x ∨ c ≤ x

case neg
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ b
x : α
hc : ¬c ≤ x
⊢ a ≤ x ∧ x < b ∨ c ≤ x ↔ a ≤ x ∨ c ≤ x

Proof state:
case h
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ b
x : α
⊢ x ∈ Ico a b ∪ Ici c ↔ x ∈ Ici (a ⊓ c)

Tactic:
simp_rw [mem_union, mem_Ico, mem_Ici, min_le_iff]

Result:
case h
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ b
x : α
⊢ a ≤ x ∧ x < b ∨ c ≤ x ↔ a ≤ x ∨ c ≤ x
-- Mathlib/Algebra/Lie/IdealOperations.lean
theorem map_comap_incl : map N.incl (comap N.incl N') = N ⊓ N'

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N N' : LieSubmodule R L M
⊢ map N.incl (comap N.incl N') = N ⊓ N'

Tactic:
rw [← toSubmodule_inj]

Result:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N N' : LieSubmodule R L M
⊢ ↑(map N.incl (comap N.incl N')) = ↑(N ⊓ N')

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N N' : LieSubmodule R L M
⊢ ↑(map N.incl (comap N.incl N')) = ↑(N ⊓ N')

Tactic:
exact (N : Submodule R M).map_comap_subtype N'

Result:
no goals
-- Mathlib/CategoryTheory/Adhesive.lean
theorem IsPushout.IsVanKampen.mono_of_mono_left [Mono f] {H : IsPushout f g h i}
    (H' : H.IsVanKampen) : Mono i :=
  IsKernelPair.mono_of_isIso_fst
    ((H' (𝟙 _) g g (𝟙 Y) (𝟙 _) f (𝟙 _) i (IsKernelPair.id_of_mono f)
        (IsPullback.of_vert_isIso ⟨by simp⟩) H.1.flip ⟨rfl⟩ ⟨by simp⟩).mp
      (IsPushout.of_horiz_isIso ⟨by simp⟩)).2

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : Mono f
H : IsPushout f g h i
H' : H.IsVanKampen
⊢ 𝟙 W ≫ g = g ≫ 𝟙 Y

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : Mono f
H : IsPushout f g h i
H' : H.IsVanKampen
⊢ g ≫ 𝟙 Y = 𝟙 W ≫ g

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem ofScientific_def : Rat.ofScientific m s e =
    if s then mkRat m (10 ^ e) else (m * 10 ^ e : Nat)

Proof state:
case false
m e : Nat
⊢ Rat.ofScientific m false e = if false = true then mkRat (↑m) (10 ^ e) else ↑(m * 10 ^ e)

case true
m e : Nat
⊢ Rat.ofScientific m true e = if true = true then mkRat (↑m) (10 ^ e) else ↑(m * 10 ^ e)

Tactic:
exact ofScientific_false_def

Result:
case true
m e : Nat
⊢ Rat.ofScientific m true e = if true = true then mkRat (↑m) (10 ^ e) else ↑(m * 10 ^ e)

Proof state:
m : Nat
s : Bool
e : Nat
⊢ Rat.ofScientific m s e = if s = true then mkRat (↑m) (10 ^ e) else ↑(m * 10 ^ e)

Tactic:
cases s

Result:
case false
m e : Nat
⊢ Rat.ofScientific m false e = if false = true then mkRat (↑m) (10 ^ e) else ↑(m * 10 ^ e)

case true
m e : Nat
⊢ Rat.ofScientific m true e = if true = true then mkRat (↑m) (10 ^ e) else ↑(m * 10 ^ e)

Proof state:
case true
m e : Nat
⊢ Rat.ofScientific m true e = if true = true then mkRat (↑m) (10 ^ e) else ↑(m * 10 ^ e)

Tactic:
exact ofScientific_true_def

Result:
no goals