harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/MvPolynomial/Tower.lean
theorem aeval_algebraMap_eq_zero_iff [NoZeroSMulDivisors A B] [Nontrivial B] (x : σ → A)
    (p : MvPolynomial σ R) : aeval (algebraMap A B ∘ x) p = 0 ↔ aeval x p = 0

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : CommSemiring B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra A B
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A B
inst✝¹ : NoZeroSMulDivisors A B
inst✝ : Nontrivial B
x : σ → A
p : MvPolynomial σ R
⊢ (aeval (⇑(algebraMap A B) ∘ x)) p = 0 ↔ (aeval x) p = 0

Tactic:
rw [aeval_algebraMap_apply, Algebra.algebraMap_eq_smul_one, smul_eq_zero,
  iff_false_intro (one_ne_zero' B), or_false]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem continuousAt_iff [PseudoMetricSpace β] {f : α → β} {a : α} :
    ContinuousAt f a ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, dist x a < δ → dist (f x) (f a) < ε

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
a : α
⊢ ContinuousAt f a ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, dist x a < δ → dist (f x) (f a) < ε

Tactic:
rw [ContinuousAt, tendsto_nhds_nhds]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean
theorem tan_angle_mul_dist_of_angle_eq_pi_div_two {p₁ p₂ p₃ : P} (h : ∠ p₁ p₂ p₃ = π / 2)
    (h0 : p₁ = p₂ ∨ p₃ ≠ p₂) : Real.tan (∠ p₂ p₃ p₁) * dist p₃ p₂ = dist p₁ p₂

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
h0 : p₁ = p₂ ∨ p₃ ≠ p₂
⊢ Real.tan (∠ p₂ p₃ p₁) * dist p₃ p₂ = dist p₁ p₂

Tactic:
rw [angle, ← inner_eq_zero_iff_angle_eq_pi_div_two, real_inner_comm, ← neg_eq_zero, ←
  inner_neg_left, neg_vsub_eq_vsub_rev] at h

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₁ = p₂ ∨ p₃ ≠ p₂
⊢ Real.tan (∠ p₂ p₃ p₁) * dist p₃ p₂ = dist p₁ p₂

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₁ = p₂ ∨ p₃ ≠ p₂
⊢ Real.tan (∠ p₂ p₃ p₁) * dist p₃ p₂ = dist p₁ p₂

Tactic:
rw [ne_comm, ← @vsub_ne_zero V, ← @vsub_eq_zero_iff_eq V, or_comm] at h0

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₂ -ᵥ p₃ ≠ 0 ∨ p₁ -ᵥ p₂ = 0
⊢ Real.tan (∠ p₂ p₃ p₁) * dist p₃ p₂ = dist p₁ p₂

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₂ -ᵥ p₃ ≠ 0 ∨ p₁ -ᵥ p₂ = 0
⊢ Real.tan (∠ p₂ p₃ p₁) * dist p₃ p₂ = dist p₁ p₂

Tactic:
rw [angle, dist_eq_norm_vsub V p₁ p₂, dist_eq_norm_vsub' V p₃ p₂, ← vsub_add_vsub_cancel p₁ p₂ p₃,
  add_comm, tan_angle_add_mul_norm_of_inner_eq_zero h h0]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem Bool.or_eq_of_eq_false_left {a b : Bool} (h : a = false) : (a || b) = b

Proof state:
a b : Bool
h : a = false
⊢ (a || b) = b

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Data/Fintype/Card.lean
theorem Fintype.card_compl_set [Fintype α] (s : Set α) [Fintype s] [Fintype (↥sᶜ : Sort _)] :
    Fintype.card (↥sᶜ : Sort _) = Fintype.card α - Fintype.card s

Proof state:
α : Type u_1
inst✝² : Fintype α
s : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑sᶜ
⊢ card ↑sᶜ = card α - card ↑s

Tactic:
rw [← Set.toFinset_card, ← Set.toFinset_card, ← Finset.card_compl, Set.toFinset_compl]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Fintype α
s : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑sᶜ
⊢ card ↑sᶜ = card α - card ↑s

Tactic:
classical rw [← Set.toFinset_card, ← Set.toFinset_card, ← Finset.card_compl, Set.toFinset_compl]

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Monoidal/Symmetric.lean
theorem braiding_naturality {X₁ X₂ Y₁ Y₂ : ModuleCat.{u} R} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) :
    (f ⊗ g) ≫ (Y₁.braiding Y₂).hom = (X₁.braiding X₂).hom ≫ (g ⊗ f)

Proof state:
case hf.H
R : Type u
inst✝ : CommRing R
X₁ X₂ Y₁ Y₂ : ModuleCat R
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
⊢ ∀ (x : ↑X₁) (y : ↑X₂),
    (Hom.hom ((f ⊗ g) ≫ (Y₁.braiding Y₂).hom)) (x ⊗ₜ[R] y) = (Hom.hom ((X₁.braiding X₂).hom ≫ (g ⊗ f))) (x ⊗ₜ[R] y)

Tactic:
intro x y

Result:
case hf.H
R : Type u
inst✝ : CommRing R
X₁ X₂ Y₁ Y₂ : ModuleCat R
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
x : ↑X₁
y : ↑X₂
⊢ (Hom.hom ((f ⊗ g) ≫ (Y₁.braiding Y₂).hom)) (x ⊗ₜ[R] y) = (Hom.hom ((X₁.braiding X₂).hom ≫ (g ⊗ f))) (x ⊗ₜ[R] y)

Proof state:
case hf.H
R : Type u
inst✝ : CommRing R
X₁ X₂ Y₁ Y₂ : ModuleCat R
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
x : ↑X₁
y : ↑X₂
⊢ (Hom.hom ((f ⊗ g) ≫ (Y₁.braiding Y₂).hom)) (x ⊗ₜ[R] y) = (Hom.hom ((X₁.braiding X₂).hom ≫ (g ⊗ f))) (x ⊗ₜ[R] y)

Tactic:
rfl

Result:
no goals

Proof state:
case hf
R : Type u
inst✝ : CommRing R
X₁ X₂ Y₁ Y₂ : ModuleCat R
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
⊢ Hom.hom ((f ⊗ g) ≫ (Y₁.braiding Y₂).hom) = Hom.hom ((X₁.braiding X₂).hom ≫ (g ⊗ f))

Tactic:
apply TensorProduct.ext'

Result:
case hf.H
R : Type u
inst✝ : CommRing R
X₁ X₂ Y₁ Y₂ : ModuleCat R
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
⊢ ∀ (x : ↑X₁) (y : ↑X₂),
    (Hom.hom ((f ⊗ g) ≫ (Y₁.braiding Y₂).hom)) (x ⊗ₜ[R] y) = (Hom.hom ((X₁.braiding X₂).hom ≫ (g ⊗ f))) (x ⊗ₜ[R] y)

Proof state:
R : Type u
inst✝ : CommRing R
X₁ X₂ Y₁ Y₂ : ModuleCat R
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
⊢ (f ⊗ g) ≫ (Y₁.braiding Y₂).hom = (X₁.braiding X₂).hom ≫ (g ⊗ f)

Tactic:
ext : 1

Result:
case hf
R : Type u
inst✝ : CommRing R
X₁ X₂ Y₁ Y₂ : ModuleCat R
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
⊢ Hom.hom ((f ⊗ g) ≫ (Y₁.braiding Y₂).hom) = Hom.hom ((X₁.braiding X₂).hom ≫ (g ⊗ f))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem isPrefixOf_replicate {a : α} :
    isPrefixOf l (replicate n a) = (decide (l.length ≤ n) && l.all (· == a))

Proof state:
case cons.zero
α : Type u_1
inst✝ : BEq α
a h : α
t : List α
ih : ∀ {n : Nat}, t.isPrefixOf (replicate n a) = (decide (t.length ≤ n) && t.all fun x => x == a)
⊢ (h :: t).isPrefixOf (replicate 0 a) = (decide ((h :: t).length ≤ 0) && (h :: t).all fun x => x == a)

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : BEq α
a h : α
t : List α
ih : ∀ {n : Nat}, t.isPrefixOf (replicate n a) = (decide (t.length ≤ n) && t.all fun x => x == a)
n : Nat
⊢ (h :: t).isPrefixOf (replicate n a) = (decide ((h :: t).length ≤ n) && (h :: t).all fun x => x == a)

Tactic:
cases n

Result:
case cons.zero
α : Type u_1
inst✝ : BEq α
a h : α
t : List α
ih : ∀ {n : Nat}, t.isPrefixOf (replicate n a) = (decide (t.length ≤ n) && t.all fun x => x == a)
⊢ (h :: t).isPrefixOf (replicate 0 a) = (decide ((h :: t).length ≤ 0) && (h :: t).all fun x => x == a)

case cons.succ
α : Type u_1
inst✝ : BEq α
a h : α
t : List α
ih : ∀ {n : Nat}, t.isPrefixOf (replicate n a) = (decide (t.length ≤ n) && t.all fun x => x == a)
n✝ : Nat
⊢ (h :: t).isPrefixOf (replicate (n✝ + 1) a) = (decide ((h :: t).length ≤ n✝ + 1) && (h :: t).all fun x => x == a)

Proof state:
case cons.succ
α : Type u_1
inst✝ : BEq α
a h : α
t : List α
ih : ∀ {n : Nat}, t.isPrefixOf (replicate n a) = (decide (t.length ≤ n) && t.all fun x => x == a)
n✝ : Nat
⊢ (h :: t).isPrefixOf (replicate (n✝ + 1) a) = (decide ((h :: t).length ≤ n✝ + 1) && (h :: t).all fun x => x == a)

Tactic:
simp [replicate_succ, isPrefixOf_cons₂, ih, Nat.succ_le_succ_iff, Bool.and_left_comm]

Result:
no goals

Proof state:
case nil
α : Type u_1
inst✝ : BEq α
a : α
n : Nat
⊢ [].isPrefixOf (replicate n a) = (decide ([].length ≤ n) && [].all fun x => x == a)

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem coe_injective : Function.Injective (Coe.coe : R[X] → PowerSeries R) := fun x y h => by
  ext
  simp_rw [← coeff_coe]
  congr

Proof state:
R : Type u_1
inst✝ : CommSemiring R
x y : R[X]
h : Coe.coe x = Coe.coe y
⊢ x = y

Tactic:
ext

Result:
case a
R : Type u_1
inst✝ : CommSemiring R
x y : R[X]
h : Coe.coe x = Coe.coe y
n✝ : ℕ
⊢ x.coeff n✝ = y.coeff n✝

Proof state:
case a
R : Type u_1
inst✝ : CommSemiring R
x y : R[X]
h : Coe.coe x = Coe.coe y
n✝ : ℕ
⊢ x.coeff n✝ = y.coeff n✝

Tactic:
simp_rw [← coeff_coe]

Result:
case a
R : Type u_1
inst✝ : CommSemiring R
x y : R[X]
h : Coe.coe x = Coe.coe y
n✝ : ℕ
⊢ (PowerSeries.coeff R n✝) ↑x = (PowerSeries.coeff R n✝) ↑y

Proof state:
case a
R : Type u_1
inst✝ : CommSemiring R
x y : R[X]
h : Coe.coe x = Coe.coe y
n✝ : ℕ
⊢ (PowerSeries.coeff R n✝) ↑x = (PowerSeries.coeff R n✝) ↑y

Tactic:
congr

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_emb_domain' {f : α → β} (hf : Injective f) [DecidablePred (· ∈ Set.range f)]
    (g : α → M) :
    (∏ᶠ b : β, if h : b ∈ Set.range f then g (Classical.choose h) else 1) = ∏ᶠ a : α, g a

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
f : α → β
hf : Injective f
inst✝ : DecidablePred fun x => x ∈ range f
g : α → M
⊢ (∏ᶠ (b : β), if h : b ∈ range f then g (Classical.choose h) else 1) = ∏ᶠ (a : α), g a

Tactic:
simp_rw [← finprod_eq_dif]

Result:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
f : α → β
hf : Injective f
inst✝ : DecidablePred fun x => x ∈ range f
g : α → M
⊢ ∏ᶠ (b : β) (h : b ∈ range f), g (Classical.choose h) = ∏ᶠ (a : α), g a

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
f : α → β
hf : Injective f
inst✝ : DecidablePred fun x => x ∈ range f
g : α → M
⊢ ∀ (a : α), (if h' : f a ∈ range f then g (Classical.choose h') else 1) = g a

Tactic:
intro a

Result:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
f : α → β
hf : Injective f
inst✝ : DecidablePred fun x => x ∈ range f
g : α → M
a : α
⊢ (if h' : f a ∈ range f then g (Classical.choose h') else 1) = g a

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
f : α → β
hf : Injective f
inst✝ : DecidablePred fun x => x ∈ range f
g : α → M
a : α
⊢ (if h' : f a ∈ range f then g (Classical.choose h') else 1) = g a

Tactic:
rw [dif_pos (Set.mem_range_self a), hf (Classical.choose_spec (Set.mem_range_self a))]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
f : α → β
hf : Injective f
inst✝ : DecidablePred fun x => x ∈ range f
g : α → M
⊢ ∏ᶠ (b : β) (h : b ∈ range f), g (Classical.choose h) = ∏ᶠ (a : α), g a

Tactic:
rw [finprod_dmem, finprod_mem_range hf, finprod_congr fun a => _]

Result:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
f : α → β
hf : Injective f
inst✝ : DecidablePred fun x => x ∈ range f
g : α → M
⊢ ∀ (a : α), (if h' : f a ∈ range f then g (Classical.choose h') else 1) = g a
-- Mathlib/.lake/packages/batteries/Batteries/Data/UnionFind/Basic.lean
theorem find_size (self : UnionFind) (x : Fin self.size) :
    (self.find x).1.size = self.size

Proof state:
self : UnionFind
x : Fin self.size
⊢ (self.find x).fst.size = self.size

Tactic:
simp [find, size, FindAux.size_eq]

Result:
no goals
-- Mathlib/Control/Traversable/Instances.lean
theorem Option.comp_traverse {α β γ} (f : β → F γ) (g : α → G β) (x : Option α) :
    Option.traverse (Comp.mk ∘ (f <$> ·) ∘ g) x =
      Comp.mk (Option.traverse f <$> Option.traverse g x)

Proof state:
case some
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
val✝ : α
⊢ Option.traverse (Comp.mk ∘ (fun x => f <$> x) ∘ g) (some val✝) =
    Comp.mk (Option.traverse f <$> Option.traverse g (some val✝))

Tactic:
simp! [functor_norm] <;> rfl

Result:
no goals

Proof state:
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
x : Option α
⊢ Option.traverse (Comp.mk ∘ (fun x => f <$> x) ∘ g) x = Comp.mk (Option.traverse f <$> Option.traverse g x)

Tactic:
cases x <;> (simp! [functor_norm] <;> rfl)

Result:
no goals
-- Mathlib/ModelTheory/Substructures.lean
theorem closure_withConstants_eq :
    closure (L[[A]]) s =
      (closure L (A ∪ s)).withConstants ((A.subset_union_left).trans subset_closure)

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
A s : Set M
⊢ (L.lhomWithConstants ↑A).substructureReduct (((closure L).toFun (A ∪ s)).withConstants ⋯) ≤
    (L.lhomWithConstants ↑A).substructureReduct ((closure (L[[↑A]])).toFun s)

Tactic:
simp only [subset_closure, reduct_withConstants, closure_le, LHom.coe_substructureReduct,
  Set.union_subset_iff, and_true]

Result:
L : Language
M : Type w
inst✝ : L.Structure M
A s : Set M
⊢ A ⊆ ↑((closure (L[[↑A]])).toFun s)

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
A s : Set M
⊢ (closure (L[[↑A]])).toFun s = ((closure L).toFun (A ∪ s)).withConstants ⋯

Tactic:
refine closure_eq_of_le ((A.subset_union_right).trans subset_closure) ?_

Result:
L : Language
M : Type w
inst✝ : L.Structure M
A s : Set M
⊢ ((closure L).toFun (A ∪ s)).withConstants ⋯ ≤ (closure (L[[↑A]])).toFun s

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
A s : Set M
⊢ A ⊆ ↑((closure (L[[↑A]])).toFun s)

Tactic:
exact subset_closure_withConstants

Result:
no goals

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
A s : Set M
⊢ ((closure L).toFun (A ∪ s)).withConstants ⋯ ≤ (closure (L[[↑A]])).toFun s

Tactic:
rw [← (L.lhomWithConstants A).substructureReduct.le_iff_le]

Result:
L : Language
M : Type w
inst✝ : L.Structure M
A s : Set M
⊢ (L.lhomWithConstants ↑A).substructureReduct (((closure L).toFun (A ∪ s)).withConstants ⋯) ≤
    (L.lhomWithConstants ↑A).substructureReduct ((closure (L[[↑A]])).toFun s)
-- Mathlib/Order/SupClosed.lean
@[simp] lemma infClosed_singleton : InfClosed ({a} : Set α)

Proof state:
α : Type u_3
inst✝ : SemilatticeInf α
a : α
⊢ InfClosed {a}

Tactic:
simp [InfClosed]

Result:
no goals
-- Mathlib/CategoryTheory/ComposableArrows.lean
@[simp]
lemma map_zero_zero : map F f 0 0 (by simp) = 𝟙 X := rfl

Proof state:
C : Type u_1
inst✝ : Category.{?u.84346, u_1} C
n m : ℕ
F G : ComposableArrows C n
X : C
f : X ⟶ F.left
⊢ 0 ≤ 0

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
lemma succAbove_lt_iff_succ_le (p : Fin (n + 1)) (i : Fin n) :
    p.succAbove i < p ↔ succ i ≤ p

Proof state:
n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ p.succAbove i < p ↔ i.succ ≤ p

Tactic:
rw [succAbove_lt_iff_castSucc_lt, castSucc_lt_iff_succ_le]

Result:
no goals
-- Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean
theorem _root_.aestronglyMeasurable_const_smul_iff (c : G) :
    AEStronglyMeasurable (fun x => c • f x) μ ↔ AEStronglyMeasurable f μ :=
  ⟨fun h => by simpa only [inv_smul_smul] using h.const_smul' c⁻¹, fun h => h.const_smul c⟩

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
G : Type u_6
inst✝² : Group G
inst✝¹ : MulAction G β
inst✝ : ContinuousConstSMul G β
c : G
h : AEStronglyMeasurable (fun x => c • f x) μ
⊢ AEStronglyMeasurable f μ

Tactic:
simpa only [inv_smul_smul] using h.const_smul' c⁻¹

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem tdiv_eq_of_eq_mul_right {a b c : Int}
    (H1 : b ≠ 0) (H2 : a = b * c) : a.tdiv b = c

Proof state:
a b c : Int
H1 : b ≠ 0
H2 : a = b * c
⊢ a.tdiv b = c

Tactic:
rw [H2, Int.mul_tdiv_cancel_left _ H1]

Result:
no goals
-- Mathlib/Algebra/Ring/SumsOfSquares.lean
theorem IsSquare.isSumSq [AddZeroClass R] [Mul R] {x : R} (hx : IsSquare x) :
    IsSumSq x

Proof state:
case intro
R : Type u_1
inst✝¹ : AddZeroClass R
inst✝ : Mul R
w✝ : R
⊢ IsSumSq (w✝ * w✝)

Tactic:
apply IsSumSq.mul_self

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : AddZeroClass R
inst✝ : Mul R
x : R
hx : IsSquare x
⊢ IsSumSq x

Tactic:
rcases hx with ⟨_, rfl⟩

Result:
case intro
R : Type u_1
inst✝¹ : AddZeroClass R
inst✝ : Mul R
w✝ : R
⊢ IsSumSq (w✝ * w✝)
-- Mathlib/Topology/MetricSpace/PiNat.lean
theorem firstDiff_comm (x y : ∀ n, E n) : firstDiff x y = firstDiff y x

Proof state:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
⊢ firstDiff x y = firstDiff y x

Tactic:
classical
simp only [firstDiff_def, ne_comm]

Result:
no goals

Proof state:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
⊢ firstDiff x y = firstDiff y x

Tactic:
simp only [firstDiff_def, ne_comm]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem isInt_rpow_pos {a b : ℝ} {nb ne : ℕ}
    (pb : IsNat b nb) (pe' : IsInt (a ^ nb) (Int.negOfNat ne)) :
    IsInt (a ^ b) (Int.negOfNat ne)

Proof state:
a b : ℝ
nb ne : ℕ
pb : IsNat b nb
pe' : IsInt (a ^ nb) (Int.negOfNat ne)
⊢ IsInt (a ^ b) (Int.negOfNat ne)

Tactic:
rwa [pb.out, rpow_natCast]

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Inversion.lean
theorem isReflection_simple (i : B) : cs.IsReflection (s i)

Proof state:
case h
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
⊢ cs.simple i = 1 * cs.simple i * 1⁻¹

Tactic:
simp

Result:
no goals

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
⊢ cs.IsReflection (cs.simple i)

Tactic:
use 1, i

Result:
case h
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
⊢ cs.simple i = 1 * cs.simple i * 1⁻¹
-- Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
theorem oneCocycles_map_one (f : oneCocycles A) : f 1 = 0

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : ↥(oneCocycles A)
this : (A.ρ 1) (f 1) - f (1 * 1) + f 1 = 0
⊢ f 1 = 0

Tactic:
simpa only [map_one, LinearMap.one_apply, mul_one, sub_self, zero_add] using this

Result:
no goals

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : ↥(oneCocycles A)
⊢ f 1 = 0

Tactic:
have := (mem_oneCocycles_def f).1 f.2 1 1

Result:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : ↥(oneCocycles A)
this : (A.ρ 1) (f 1) - f (1 * 1) + f 1 = 0
⊢ f 1 = 0
-- Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean
theorem measure_eq_iInf' (μ : Measure α) (s : Set α) :
    μ s = ⨅ t : { t // s ⊆ t ∧ MeasurableSet t }, μ t

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
⊢ μ s = ⨅ t, μ ↑t

Tactic:
simp_rw [iInf_subtype, iInf_and, ← measure_eq_iInf]

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean
protected lemma le_of_add_le_add_left [LE α] [AddLeftReflectLE α] (hx : x ≠ ⊤) :
    x + y ≤ x + z → y ≤ z

Proof state:
α : Type u
inst✝² : Add α
x y z : WithTop α
inst✝¹ : LE α
inst✝ : AddLeftReflectLE α
hx : x ≠ ⊤
⊢ x + y ≤ x + z → y ≤ z

Tactic:
lift x to α using hx

Result:
case intro
α : Type u
inst✝² : Add α
y z : WithTop α
inst✝¹ : LE α
inst✝ : AddLeftReflectLE α
x : α
⊢ ↑x + y ≤ ↑x + z → y ≤ z

Proof state:
case intro.coe.coe
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : AddLeftReflectLE α
x a✝¹ a✝ : α
⊢ x + a✝¹ ≤ x + a✝ → a✝¹ ≤ a✝

Tactic:
simpa using le_of_add_le_add_left

Result:
no goals

Proof state:
case intro
α : Type u
inst✝² : Add α
y z : WithTop α
inst✝¹ : LE α
inst✝ : AddLeftReflectLE α
x : α
⊢ ↑x + y ≤ ↑x + z → y ≤ z

Tactic:
cases y <;> cases z <;> simp [← coe_add]

Result:
case intro.coe.coe
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : AddLeftReflectLE α
x a✝¹ a✝ : α
⊢ x + a✝¹ ≤ x + a✝ → a✝¹ ≤ a✝
-- Mathlib/CategoryTheory/NatIso.lean
theorem cancel_natIso_hom_right_assoc {W X X' : D} {Y : C} (f : W ⟶ X) (g : X ⟶ F.obj Y)
    (f' : W ⟶ X') (g' : X' ⟶ F.obj Y) :
    f ≫ g ≫ α.hom.app Y = f' ≫ g' ≫ α.hom.app Y ↔ f ≫ g = f' ≫ g'

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
W X X' : D
Y : C
f : W ⟶ X
g : X ⟶ F.obj Y
f' : W ⟶ X'
g' : X' ⟶ F.obj Y
⊢ f ≫ g ≫ α.hom.app Y = f' ≫ g' ≫ α.hom.app Y ↔ f ≫ g = f' ≫ g'

Tactic:
simp only [← Category.assoc, cancel_mono, refl]

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialNerve.lean
@[simp]
lemma comp_id (i j : SimplicialThickening J) :
    (ρ_ (Hom i j)).inv ≫ Hom i j ◁ id j ≫ comp i j j = 𝟙 (Hom i j)

Proof state:
J : Type u_1
inst✝ : LinearOrder J
i j : SimplicialThickening J
n✝ : SimplexCategoryᵒᵖ
a✝ : (Hom i j ⊗ 𝟙_ SSet).obj n✝
x✝ : Fin ((Opposite.unop n✝).len + 1)
⊢ ((Hom i j ◁ id j ≫ comp i j j).app n✝ a✝).obj x✝ = (((ρ_ (Hom i j)).hom ≫ 𝟙 (Hom i j)).app n✝ a✝).obj x✝

Tactic:
simp

Result:
no goals

Proof state:
case w.h
J : Type u_1
inst✝ : LinearOrder J
i j : SimplicialThickening J
n✝ : SimplexCategoryᵒᵖ
a✝ : (Hom i j ⊗ 𝟙_ SSet).obj n✝
⊢ (Hom i j ◁ id j ≫ comp i j j).app n✝ a✝ = ((ρ_ (Hom i j)).hom ≫ 𝟙 (Hom i j)).app n✝ a✝

Tactic:
exact Functor.ext (fun _ ↦ by simp)

Result:
no goals

Proof state:
J : Type u_1
inst✝ : LinearOrder J
i j : SimplicialThickening J
⊢ (ρ_ (Hom i j)).inv ≫ Hom i j ◁ id j ≫ comp i j j = 𝟙 (Hom i j)

Tactic:
rw [Iso.inv_comp_eq]

Result:
J : Type u_1
inst✝ : LinearOrder J
i j : SimplicialThickening J
⊢ Hom i j ◁ id j ≫ comp i j j = (ρ_ (Hom i j)).hom ≫ 𝟙 (Hom i j)

Proof state:
J : Type u_1
inst✝ : LinearOrder J
i j : SimplicialThickening J
⊢ Hom i j ◁ id j ≫ comp i j j = (ρ_ (Hom i j)).hom ≫ 𝟙 (Hom i j)

Tactic:
ext

Result:
case w.h
J : Type u_1
inst✝ : LinearOrder J
i j : SimplicialThickening J
n✝ : SimplexCategoryᵒᵖ
a✝ : (Hom i j ⊗ 𝟙_ SSet).obj n✝
⊢ (Hom i j ◁ id j ≫ comp i j j).app n✝ a✝ = ((ρ_ (Hom i j)).hom ≫ 𝟙 (Hom i j)).app n✝ a✝
-- Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean
@[simp]
lemma const_eq_id : const ⦋0⦌ ⦋0⦌ 0 = 𝟙 _

Proof state:
⊢ ⦋0⦌.const ⦋0⦌ 0 = 𝟙 ⦋0⦌

Tactic:
aesop

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Iio_union_Ico (h : min c d ≤ b) : Iio b ∪ Ico c d = Iio (max b d)

Proof state:
case inl
α : Type u_1
inst✝ : LinearOrder α
b c d : α
hcd : c ≤ d
h : c ≤ b
⊢ Iio b ∪ Ico c d = Iio (b ⊔ d)

Tactic:
exact Iio_union_Ico' h

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
b c d : α
h : c ⊓ d ≤ b
⊢ Iio b ∪ Ico c d = Iio (b ⊔ d)

Tactic:
rcases le_total c d with hcd | hcd <;> simp [hcd] at h

Result:
case inl
α : Type u_1
inst✝ : LinearOrder α
b c d : α
hcd : c ≤ d
h : c ≤ b
⊢ Iio b ∪ Ico c d = Iio (b ⊔ d)

case inr
α : Type u_1
inst✝ : LinearOrder α
b c d : α
hcd : d ≤ c
h : d ≤ b
⊢ Iio b ∪ Ico c d = Iio (b ⊔ d)

Proof state:
case inr
α : Type u_1
inst✝ : LinearOrder α
b c d : α
hcd : d ≤ c
h : d ≤ b
⊢ Iio b ∪ Ico c d = Iio (b ⊔ d)

Tactic:
simp [*]

Result:
no goals
-- Mathlib/RingTheory/Generators.lean
lemma toComp_toAlgHom_monomial (Q : Generators S T) (P : Generators R S) (j a) :
    (Q.toComp P).toAlgHom (monomial j a) =
      monomial (Finsupp.sumElim 0 j) a

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
j : P.vars →₀ ℕ
a : R
⊢ (Q.toComp P).toAlgHom ((monomial j) a) = (monomial (Finsupp.sumElim 0 j)) a

Tactic:
convert rename_monomial _ _ _

Result:
case h.e'_3.h.e'_5.h.h.e'_4.h.h.e
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
j : P.vars →₀ ℕ
a : R
e_1✝ : (R →ₗ[R] MvPolynomial (Q.vars ⊕ P.vars) R) = (R →ₗ[R] MvPolynomial (Q.comp P).vars R)
e_2✝ : (Q.vars ⊕ P.vars) = (Q.comp P).vars
⊢ Finsupp.sumElim 0 = Finsupp.mapDomain Sum.inr

Proof state:
case h.e'_3.h.e'_5.h.h.e'_4.h.h.e
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
j : P.vars →₀ ℕ
a : R
e_1✝ : (R →ₗ[R] MvPolynomial (Q.vars ⊕ P.vars) R) = (R →ₗ[R] MvPolynomial (Q.comp P).vars R)
e_2✝ : (Q.vars ⊕ P.vars) = (Q.comp P).vars
⊢ Finsupp.sumElim 0 = Finsupp.mapDomain Sum.inr

Tactic:
ext f (i₁ | i₂) <;>
  simp [Finsupp.mapDomain_notin_range, Finsupp.mapDomain_apply Sum.inr_injective]

Result:
no goals