harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Tactic/NormNum/RealSqrt.lean
lemma isRat_realSqrt_of_isRat_ofNat {x : ℝ} {n sn : ℕ} {d sd : ℕ} (hn : sn * sn = n)
    (hd : sd * sd = d) (h : IsRat x (.ofNat n) d) :
    IsRat √x (.ofNat sn) sd

Proof state:
case mk
n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
inv✝ : Invertible ↑d
⊢ Invertible ↑sd

Tactic:
apply invertibleOfNonzero

Result:
case mk.h
n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
inv✝ : Invertible ↑d
⊢ ↑sd ≠ 0

Proof state:
case mk.h
n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
inv✝ : Invertible ↑d
⊢ ↑sd ≠ 0

Tactic:
rw [← mul_self_ne_zero, ← Nat.cast_mul, hd]

Result:
case mk.h
n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
inv✝ : Invertible ↑d
⊢ ↑d ≠ 0

Proof state:
x : ℝ
n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
h : IsRat x (Int.ofNat n) d
⊢ IsRat (√x) (Int.ofNat sn) sd

Tactic:
obtain ⟨_, rfl⟩ := h

Result:
case mk
n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
inv✝ : Invertible ↑d
⊢ IsRat (√(↑(Int.ofNat n) * ⅟↑d)) (Int.ofNat sn) sd

Proof state:
case out
n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
inv✝ : Invertible ↑d
⊢ √(↑(Int.ofNat n) * ⅟↑d) = ↑(Int.ofNat sn) * ⅟↑sd

Tactic:
simp [← hn, ← hd, Real.sqrt_mul (mul_self_nonneg ↑sn)]

Result:
no goals

Proof state:
case mk.h
n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
inv✝ : Invertible ↑d
⊢ ↑d ≠ 0

Tactic:
exact Invertible.ne_zero _

Result:
no goals

Proof state:
case mk
n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
inv✝ : Invertible ↑d
⊢ IsRat (√(↑(Int.ofNat n) * ⅟↑d)) (Int.ofNat sn) sd

Tactic:
refine ⟨?_, ?out⟩

Result:
case mk
n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
inv✝ : Invertible ↑d
⊢ Invertible ↑sd

case out
n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
inv✝ : Invertible ↑d
⊢ √(↑(Int.ofNat n) * ⅟↑d) = ↑(Int.ofNat sn) * ⅟↑sd
-- Mathlib/MeasureTheory/Integral/IntervalAverage.lean
theorem interval_average_eq_div (f : ℝ → ℝ) (a b : ℝ) :
    (⨍ x in a..b, f x) = (∫ x in a..b, f x) / (b - a)

Proof state:
f : ℝ → ℝ
a b : ℝ
⊢ ⨍ (x : ℝ) in a..b, f x = (∫ (x : ℝ) in a..b, f x) / (b - a)

Tactic:
rw [interval_average_eq, smul_eq_mul, div_eq_inv_mul]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
@[simp]
lemma inr_snd_assoc {K : CochainComplex C ℤ} {d e : ℤ} (γ : Cochain G K d) (he : 0 + d = e) :
    (Cochain.ofHom (inr φ)).comp ((snd φ).comp γ he) (by simp only [← he, zero_add]) = γ

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{?u.51796, u_1} C
inst✝³ : Category.{?u.51800, u_2} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
d e : ℤ
γ : Cochain G K d
he : 0 + d = e
⊢ 0 + e = d

Tactic:
simp only [← he, zero_add]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
d e : ℤ
γ : Cochain G K d
he : 0 + d = e
⊢ (Cochain.ofHom (inr φ)).comp ((snd φ).comp γ he) ⋯ = γ

Tactic:
obtain rfl : d = e := by omega

Result:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
d : ℤ
γ : Cochain G K d
he : 0 + d = d
⊢ (Cochain.ofHom (inr φ)).comp ((snd φ).comp γ he) ⋯ = γ

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
d : ℤ
γ : Cochain G K d
he : 0 + d = d
⊢ (Cochain.ofHom (inr φ)).comp ((snd φ).comp γ he) ⋯ = γ

Tactic:
rw [← Cochain.comp_assoc_of_first_is_zero_cochain, inr_snd, Cochain.id_comp]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
d e : ℤ
γ : Cochain G K d
he : 0 + d = e
⊢ d = e

Tactic:
omega

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryBiproducts.lean
theorem isIso_right_of_isIso_biprod_map {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z)
    [IsIso (biprod.map f g)] : IsIso g :=
  letI : IsIso (biprod.map g f)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝ : IsIso (biprod.map f g)
⊢ IsIso (biprod.map g f)

Tactic:
rw [← biprod.braiding_map_braiding]

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝ : IsIso (biprod.map f g)
⊢ IsIso ((biprod.braiding X W).hom ≫ biprod.map f g ≫ (biprod.braiding Y Z).hom)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝ : IsIso (biprod.map f g)
⊢ IsIso ((biprod.braiding X W).hom ≫ biprod.map f g ≫ (biprod.braiding Y Z).hom)

Tactic:
infer_instance

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem size_pmap {p : α → Prop} {f : ∀ a, p a → β} {l H} : (pmap f l H).size = l.size

Proof state:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
toList✝ : List α
H : ∀ (a : α), a ∈ { toList := toList✝ } → p a
⊢ (pmap f { toList := toList✝ } H).size = { toList := toList✝ }.size

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
l : Array α
H : ∀ (a : α), a ∈ l → p a
⊢ (pmap f l H).size = l.size

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
toList✝ : List α
H : ∀ (a : α), a ∈ { toList := toList✝ } → p a
⊢ (pmap f { toList := toList✝ } H).size = { toList := toList✝ }.size
-- Mathlib/CategoryTheory/Abelian/NonPreadditive.lean
theorem add_neg_cancel {X Y : C} (a : X ⟶ Y) : a + -a = 0

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
⊢ a + -a = 0

Tactic:
rw [add_neg, sub_self]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem findIdx_eq_getD_findIdx? {xs : Array α} {p : α → Bool} :
    xs.findIdx p = (xs.findIdx? p).getD xs.size

Proof state:
α : Type u_1
xs : Array α
p : α → Bool
⊢ findIdx p xs = (findIdx? p xs).getD xs.size

Tactic:
rcases xs with ⟨xs⟩

Result:
case mk
α : Type u_1
p : α → Bool
xs : List α
⊢ findIdx p { toList := xs } = (findIdx? p { toList := xs }).getD { toList := xs }.size

Proof state:
case mk
α : Type u_1
p : α → Bool
xs : List α
⊢ findIdx p { toList := xs } = (findIdx? p { toList := xs }).getD { toList := xs }.size

Tactic:
simp [List.findIdx_eq_getD_findIdx?]

Result:
no goals
-- Mathlib/Algebra/Lie/Solvable.lean
theorem derivedSeries_eq_bot_iff (k : ℕ) :
    derivedSeries R I k = ⊥ ↔ derivedSeriesOfIdeal R L k I = ⊥

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
⊢ derivedSeries R (↥I) k = ⊥ ↔ derivedSeriesOfIdeal R L k I = ⊥

Tactic:
rw [← derivedSeries_eq_derivedSeriesOfIdeal_map, map_eq_bot_iff, ker_incl, eq_bot_iff]

Result:
no goals
-- Mathlib/RingTheory/Smooth/StandardSmooth.lean
@[simp]
lemma aevalDifferential_single [DecidableEq P.rels] (i j : P.rels) :
    P.aevalDifferential (Pi.single i 1) j = aeval P.val (pderiv (P.map j) (P.relation i))

Proof state:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : PreSubmersivePresentation R S
inst✝ : DecidableEq P.rels
i j : P.rels
⊢ P.aevalDifferential (Pi.single i 1) j = (aeval P.val) ((pderiv (P.map j)) (P.relation i))

Tactic:
dsimp only [aevalDifferential]

Result:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : PreSubmersivePresentation R S
inst✝ : DecidableEq P.rels
i j : P.rels
⊢ (((Pi.basisFun S P.rels).constr S) fun j i => (aeval P.val) ((pderiv (P.map i)) (P.relation j))) (Pi.single i 1) j =
    (aeval P.val) ((pderiv (P.map j)) (P.relation i))

Proof state:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : PreSubmersivePresentation R S
inst✝ : DecidableEq P.rels
i j : P.rels
⊢ (((Pi.basisFun S P.rels).constr S) fun j i => (aeval P.val) ((pderiv (P.map i)) (P.relation j))) (Pi.single i 1) j =
    (aeval P.val) ((pderiv (P.map j)) (P.relation i))

Tactic:
rw [← Pi.basisFun_apply, Basis.constr_basis]

Result:
no goals
-- Mathlib/Combinatorics/Colex.lean
/-- Being a nonempty initial segment of colex is equivalent to being an `initSeg`. -/
lemma isInitSeg_iff_exists_initSeg :
    IsInitSeg 𝒜 r ∧ 𝒜.Nonempty ↔ ∃ s : Finset α, #s = r ∧ 𝒜 = initSeg s

Proof state:
case intro.intro
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Fintype α
s : Finset α
⊢ IsInitSeg (initSeg s) #s ∧ (initSeg s).Nonempty

Tactic:
exact ⟨isInitSeg_initSeg, initSeg_nonempty⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
⊢ (∃ s, #s = r ∧ 𝒜 = initSeg s) → IsInitSeg 𝒜 r ∧ 𝒜.Nonempty

Tactic:
rintro ⟨s, rfl, rfl⟩

Result:
case intro.intro
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Fintype α
s : Finset α
⊢ IsInitSeg (initSeg s) #s ∧ (initSeg s).Nonempty

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
⊢ IsInitSeg 𝒜 r ∧ 𝒜.Nonempty ↔ ∃ s, #s = r ∧ 𝒜 = initSeg s

Tactic:
refine ⟨fun h𝒜 ↦ h𝒜.1.exists_initSeg h𝒜.2, ?_⟩

Result:
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
⊢ (∃ s, #s = r ∧ 𝒜 = initSeg s) → IsInitSeg 𝒜 r ∧ 𝒜.Nonempty
-- Mathlib/CategoryTheory/GradedObject/Monoidal.lean
lemma tensorHom_def {X₁ X₂ Y₁ Y₂ : GradedObject I C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂)
    [HasTensor X₁ Y₁] [HasTensor X₂ Y₂] [HasTensor X₂ Y₁] :
    tensorHom f g = whiskerRight f Y₁ ≫ whiskerLeft X₂ g

Proof state:
I : Type u
inst✝⁵ : AddMonoid I
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : MonoidalCategory C
X₁ X₂ Y₁ Y₂ : GradedObject I C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
inst✝² : X₁.HasTensor Y₁
inst✝¹ : X₂.HasTensor Y₂
inst✝ : X₂.HasTensor Y₁
⊢ tensorHom f g = whiskerRight f Y₁ ≫ whiskerLeft X₂ g

Tactic:
rw [← tensor_comp, id_comp, comp_id]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_smul_right_of_neg (x y : V) {r : ℝ} (hr : r < 0) :
    o.oangle x (r • y) = o.oangle x (-y)

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
hr : r < 0
⊢ o.oangle x (r • y) = o.oangle x (-y)

Tactic:
rw [← neg_neg r, neg_smul, ← smul_neg, o.oangle_smul_right_of_pos _ _ (neg_pos_of_neg hr)]

Result:
no goals
-- Mathlib/LinearAlgebra/Determinant.lean
theorem Basis.det_map (b : Basis ι R M) (f : M ≃ₗ[R] M') (v : ι → M') :
    (b.map f).det v = b.det (f.symm ∘ v)

Proof state:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
f : M ≃ₗ[R] M'
v : ι → M'
⊢ (b.map f).det v = b.det (⇑f.symm ∘ v)

Tactic:
rw [Basis.det_apply, Basis.toMatrix_map, Basis.det_apply]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
theorem _root_.RingHom.map_det (f : R →+* S) (M : Matrix n n R) :
    f M.det = Matrix.det (f.mapMatrix M)

Proof state:
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type w
inst✝ : CommRing S
f : R →+* S
M : Matrix n n R
⊢ f M.det = (f.mapMatrix M).det

Tactic:
simp [Matrix.det_apply', map_sum f, map_prod f]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem contains_of_contains_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {a k : α} {v : β k} :
    (m.insert k v).contains a → (k == a) = false → m.contains a

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
a k : α
v : β k
⊢ (m.insert k v).contains a = true → (k == a) = false → m.contains a = true

Tactic:
simp_to_raw using Raw₀.contains_of_contains_insert

Result:
no goals
-- Mathlib/Combinatorics/Hindman.lean
theorem FP_drop_subset_FP {M} [Semigroup M] (a : Stream' M) (n : ℕ) : FP (a.drop n) ⊆ FP a

Proof state:
case zero
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
⊢ FP (Stream'.drop 0 a) ⊆ FP a

Tactic:
rfl

Result:
no goals

Proof state:
case succ
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
n : ℕ
ih : FP (Stream'.drop n a) ⊆ FP a
⊢ FP (Stream'.drop 1 (Stream'.drop n a)) ⊆ FP a

Tactic:
exact _root_.trans (FP.tail _) ih

Result:
no goals

Proof state:
case succ
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
n : ℕ
ih : FP (Stream'.drop n a) ⊆ FP a
⊢ FP (Stream'.drop (n + 1) a) ⊆ FP a

Tactic:
rw [← Stream'.drop_drop]

Result:
case succ
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
n : ℕ
ih : FP (Stream'.drop n a) ⊆ FP a
⊢ FP (Stream'.drop 1 (Stream'.drop n a)) ⊆ FP a

Proof state:
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
n : ℕ
⊢ FP (Stream'.drop n a) ⊆ FP a

Tactic:
induction n with
| zero => rfl
| succ n ih =>
  rw [← Stream'.drop_drop]
  exact _root_.trans (FP.tail _) ih

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Control/ForInStep/Lemmas.lean
theorem ForInStep.bind_bindList_assoc [Monad m] [LawfulMonad m]
    (f : β → m (ForInStep β)) (g : α → β → m (ForInStep β)) (s : ForInStep β) (l) :
    s.bind f >>= (·.bindList g l) = s.bind fun b => f b >>= (·.bindList g l)

Proof state:
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β → m (ForInStep β)
g : α → β → m (ForInStep β)
s : ForInStep β
l : List α
⊢ (do
      let x ← s.bind f
      bindList g l x) =
    s.bind fun b => do
      let x ← f b
      bindList g l x

Tactic:
cases s <;> simp

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem tan_oangle_sub_left_mul_norm_of_oangle_eq_pi_div_two {x y : V}
    (h : o.oangle x y = ↑(π / 2)) : Real.Angle.tan (o.oangle (x - y) x) * ‖x‖ = ‖y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle (x - y) x).tan * ‖x‖ = ‖y‖

Tactic:
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ ((-o).oangle x (x - y)).tan * ‖x‖ = ‖y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ ((-o).oangle x (x - y)).tan * ‖x‖ = ‖y‖

Tactic:
exact (-o).tan_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two h

Result:
no goals
-- Mathlib/LinearAlgebra/LinearPMap.lean
theorem mkSpanSingleton'_apply_self (x : E) (y : F) (H : ∀ c : R, c • x = 0 → c • y = 0) (h) :
    mkSpanSingleton' x y H ⟨x, h⟩ = y

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
x : E
y : F
H : ∀ (c : R), c • x = 0 → c • y = 0
h : x ∈ (mkSpanSingleton' x y H).domain
⊢ 1 • x ∈ (mkSpanSingleton' x y H).domain

Tactic:
rwa [one_smul]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
x : E
y : F
H : ∀ (c : R), c • x = 0 → c • y = 0
h : x ∈ (mkSpanSingleton' x y H).domain
⊢ ↑(mkSpanSingleton' x y H) ⟨x, h⟩ = y

Tactic:
have := by refine mkSpanSingleton'_apply x y H 1 ?_; rwa [one_smul]

Result:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
x : E
y : F
H : ∀ (c : R), c • x = 0 → c • y = 0
h : x ∈ (mkSpanSingleton' x y H).domain
this : ↑(mkSpanSingleton' x y H) ⟨1 • x, ⋯⟩ = 1 • y
⊢ ↑(mkSpanSingleton' x y H) ⟨x, h⟩ = y

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
x : E
y : F
H : ∀ (c : R), c • x = 0 → c • y = 0
h : x ∈ (mkSpanSingleton' x y H).domain
⊢ ?m.39780

Tactic:
refine mkSpanSingleton'_apply x y H 1 ?_

Result:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
x : E
y : F
H : ∀ (c : R), c • x = 0 → c • y = 0
h : x ∈ (mkSpanSingleton' x y H).domain
⊢ 1 • x ∈ (mkSpanSingleton' x y H).domain

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
x : E
y : F
H : ∀ (c : R), c • x = 0 → c • y = 0
h : x ∈ (mkSpanSingleton' x y H).domain
this : ↑(mkSpanSingleton' x y H) ⟨1 • x, ⋯⟩ = 1 • y
⊢ ↑(mkSpanSingleton' x y H) ⟨x, h⟩ = y

Tactic:
convert this <;> rw [one_smul]

Result:
no goals
-- Mathlib/RingTheory/RootsOfUnity/Basic.lean
@[simp]
lemma rootsOfUnity_zero (M : Type*) [CommMonoid M] : rootsOfUnity 0 M = ⊤

Proof state:
case h
M : Type u_7
inst✝ : CommMonoid M
x✝ : Mˣ
⊢ x✝ ∈ rootsOfUnity 0 M ↔ x✝ ∈ ⊤

Tactic:
simp only [mem_rootsOfUnity, pow_zero, Subgroup.mem_top]

Result:
no goals

Proof state:
M : Type u_7
inst✝ : CommMonoid M
⊢ rootsOfUnity 0 M = ⊤

Tactic:
ext1

Result:
case h
M : Type u_7
inst✝ : CommMonoid M
x✝ : Mˣ
⊢ x✝ ∈ rootsOfUnity 0 M ↔ x✝ ∈ ⊤
-- Mathlib/Data/ENNReal/Action.lean
theorem smul_toNNReal (a : ℝ≥0) (b : ℝ≥0∞) : (a • b).toNNReal = a * b.toNNReal

Proof state:
a : ℝ≥0
b : ℝ≥0∞
⊢ (a • b).toNNReal = a * b.toNNReal

Tactic:
change ((a : ℝ≥0∞) * b).toNNReal = a * b.toNNReal

Result:
a : ℝ≥0
b : ℝ≥0∞
⊢ (↑a * b).toNNReal = a * b.toNNReal

Proof state:
a : ℝ≥0
b : ℝ≥0∞
⊢ (↑a * b).toNNReal = a * b.toNNReal

Tactic:
simp only [ENNReal.toNNReal_mul, ENNReal.toNNReal_coe]

Result:
no goals
-- Mathlib/Data/Rat/Lemmas.lean
theorem den_div_intCast_eq_one_iff (m n : ℤ) (hn : n ≠ 0) : ((m : ℚ) / n).den = 1 ↔ n ∣ m

Proof state:
case mp
m n : ℤ
hn : ↑n ≠ 0
⊢ (↑m / ↑n).den = 1 → n ∣ m

Tactic:
rw [Rat.den_eq_one_iff, eq_div_iff hn]

Result:
case mp
m n : ℤ
hn : ↑n ≠ 0
⊢ ↑(↑m / ↑n).num * ↑n = ↑m → n ∣ m

Proof state:
case mp
m n : ℤ
hn : ↑n ≠ 0
⊢ ↑(↑m / ↑n).num * ↑n = ↑m → n ∣ m

Tactic:
exact mod_cast (Dvd.intro_left _)

Result:
no goals

Proof state:
m n : ℤ
hn : n ≠ 0
⊢ (↑m / ↑n).den = 1 ↔ n ∣ m

Tactic:
replace hn : (n : ℚ) ≠ 0 := num_ne_zero.mp hn

Result:
m n : ℤ
hn : ↑n ≠ 0
⊢ (↑m / ↑n).den = 1 ↔ n ∣ m

Proof state:
m n : ℤ
hn : ↑n ≠ 0
⊢ (↑m / ↑n).den = 1 ↔ n ∣ m

Tactic:
constructor

Result:
case mp
m n : ℤ
hn : ↑n ≠ 0
⊢ (↑m / ↑n).den = 1 → n ∣ m

case mpr
m n : ℤ
hn : ↑n ≠ 0
⊢ n ∣ m → (↑m / ↑n).den = 1
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/PosPart.lean
@[simp]
lemma posPart_natCast (n : ℕ) : (n : A)⁺ = n

Proof state:
A : Type u_1
inst✝⁵ : Ring A
inst✝⁴ : Algebra ℝ A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : T2Space A
n : ℕ
⊢ (↑n)⁺ = ↑n

Tactic:
rw [← map_natCast (algebraMap ℝ≥0 A), posPart_algebraMap_nnreal]

Result:
no goals
-- Mathlib/Algebra/Quandle.lean
theorem well_def {R : Type*} [Rack R] {G : Type*} [Group G] (f : R →◃ Quandle.Conj G) :
    ∀ {a b : PreEnvelGroup R},
      PreEnvelGroupRel' R a b → toEnvelGroup.mapAux f a = toEnvelGroup.mapAux f b
  | _, _, PreEnvelGroupRel'.refl => rfl
  | _, _, PreEnvelGroupRel'.symm h => (well_def f h).symm
  | _, _, PreEnvelGroupRel'.trans hac hcb => Eq.trans (well_def f hac) (well_def f hcb)
  | _, _, PreEnvelGroupRel'.congr_mul ha hb => by
    simp [toEnvelGroup.mapAux, well_def f ha, well_def f hb]
  | _, _, congr_inv ha => by simp [toEnvelGroup.mapAux, well_def f ha]
  | _, _, assoc a b c => by apply mul_assoc
  | _, _, PreEnvelGroupRel'.one_mul a => by simp [toEnvelGroup.mapAux]
  | _, _, PreEnvelGroupRel'.mul_one a => by simp [toEnvelGroup.mapAux]
  | _, _, PreEnvelGroupRel'.inv_mul_cancel a => by simp [toEnvelGroup.mapAux]
  | _, _, act_incl x y => by simp [toEnvelGroup.mapAux]

Proof state:
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
f : R →◃ Quandle.Conj G
x y : R
⊢ mapAux f (((incl x).mul (incl y)).mul (incl x).inv) = mapAux f (incl (x ◃ y))

Tactic:
simp [toEnvelGroup.mapAux]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
f : R →◃ Quandle.Conj G
a✝ a'✝ : PreEnvelGroup R
ha : PreEnvelGroupRel' R a✝ a'✝
⊢ mapAux f a✝.inv = mapAux f a'✝.inv

Tactic:
simp [toEnvelGroup.mapAux, well_def f ha]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
f : R →◃ Quandle.Conj G
a : PreEnvelGroup R
⊢ mapAux f (unit.mul a) = mapAux f a

Tactic:
simp [toEnvelGroup.mapAux]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
f : R →◃ Quandle.Conj G
a : PreEnvelGroup R
⊢ mapAux f (a.mul unit) = mapAux f a

Tactic:
simp [toEnvelGroup.mapAux]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
f : R →◃ Quandle.Conj G
a : PreEnvelGroup R
⊢ mapAux f (a.inv.mul a) = mapAux f unit

Tactic:
simp [toEnvelGroup.mapAux]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
f : R →◃ Quandle.Conj G
a✝ b✝ a'✝ b'✝ : PreEnvelGroup R
ha : PreEnvelGroupRel' R a✝ a'✝
hb : PreEnvelGroupRel' R b✝ b'✝
⊢ mapAux f (a✝.mul b✝) = mapAux f (a'✝.mul b'✝)

Tactic:
simp [toEnvelGroup.mapAux, well_def f ha, well_def f hb]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
f : R →◃ Quandle.Conj G
a b c : PreEnvelGroup R
⊢ mapAux f ((a.mul b).mul c) = mapAux f (a.mul (b.mul c))

Tactic:
apply mul_assoc

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem isBigO_pi {ι : Type*} [Fintype ι] {E' : ι → Type*} [∀ i, NormedAddCommGroup (E' i)]
    {f : α → ∀ i, E' i} : f =O[l] g' ↔ ∀ i, (fun x => f x i) =O[l] g'

Proof state:
α : Type u_1
F' : Type u_7
inst✝² : SeminormedAddCommGroup F'
g' : α → F'
l : Filter α
ι : Type u_17
inst✝¹ : Fintype ι
E' : ι → Type u_18
inst✝ : (i : ι) → NormedAddCommGroup (E' i)
f : α → (i : ι) → E' i
⊢ (∀ᶠ (c : ℝ) in atTop, IsBigOWith c l f g') ↔ ∀ᶠ (x : ℝ) in atTop, ∀ (i : ι), IsBigOWith x l (fun x => f x i) g'

Tactic:
exact eventually_congr (eventually_atTop.2 ⟨0, fun c => isBigOWith_pi⟩)

Result:
no goals

Proof state:
α : Type u_1
F' : Type u_7
inst✝² : SeminormedAddCommGroup F'
g' : α → F'
l : Filter α
ι : Type u_17
inst✝¹ : Fintype ι
E' : ι → Type u_18
inst✝ : (i : ι) → NormedAddCommGroup (E' i)
f : α → (i : ι) → E' i
⊢ f =O[l] g' ↔ ∀ (i : ι), (fun x => f x i) =O[l] g'

Tactic:
simp only [isBigO_iff_eventually_isBigOWith, ← eventually_all]

Result:
α : Type u_1
F' : Type u_7
inst✝² : SeminormedAddCommGroup F'
g' : α → F'
l : Filter α
ι : Type u_17
inst✝¹ : Fintype ι
E' : ι → Type u_18
inst✝ : (i : ι) → NormedAddCommGroup (E' i)
f : α → (i : ι) → E' i
⊢ (∀ᶠ (c : ℝ) in atTop, IsBigOWith c l f g') ↔ ∀ᶠ (x : ℝ) in atTop, ∀ (i : ι), IsBigOWith x l (fun x => f x i) g'
-- Mathlib/Algebra/Module/Submodule/Lattice.lean
theorem disjoint_def {p p' : Submodule R M} : Disjoint p p' ↔ ∀ x ∈ p, x ∈ p' → x = (0 : M) :=
  disjoint_iff_inf_le.trans <| show (∀ x, x ∈ p ∧ x ∈ p' → x ∈ ({0} : Set M)) ↔ _ by simp

Proof state:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p p' : Submodule R M
⊢ (∀ (x : M), x ∈ p ∧ x ∈ p' → x ∈ {0}) ↔ ∀ x ∈ p, x ∈ p' → x = 0

Tactic:
simp

Result:
no goals