harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Manifold/LocalInvariantProperties.lean
theorem liftPropAt_of_liftPropWithinAt (h : LiftPropWithinAt P g s x) (hs : s ∈ 𝓝 x) :
    LiftPropAt P g x

Proof state:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
h : LiftPropWithinAt P g s x
hs : s ∈ 𝓝 x
⊢ LiftPropAt P g x

Tactic:
rwa [← univ_inter s, hG.liftPropWithinAt_inter hs] at h

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem arg_cos_add_sin_mul_I_coe_angle (θ : Real.Angle) :
    (arg (Real.Angle.cos θ + Real.Angle.sin θ * I) : Real.Angle) = θ

Proof state:
θ : Real.Angle
⊢ ↑(↑θ.cos + ↑θ.sin * I).arg = θ

Tactic:
rw [← one_mul (_ + _), ← ofReal_one, arg_mul_cos_add_sin_mul_I_coe_angle zero_lt_one]

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/TerminatedStable.lean
theorem dens_stable_of_terminated (n_le_m : n ≤ m) (terminatedAt_n : g.TerminatedAt n) :
    g.dens m = g.dens n

Proof state:
K : Type u_1
g : GenContFract K
n m : ℕ
inst✝ : DivisionRing K
n_le_m : n ≤ m
terminatedAt_n : g.TerminatedAt n
⊢ g.dens m = g.dens n

Tactic:
simp only [den_eq_conts_b, conts_stable_of_terminated n_le_m terminatedAt_n]

Result:
no goals
-- Mathlib/Data/Set/NAry.lean
theorem image2_empty_left : image2 f ∅ t = ∅ :=
  ext <| by simp

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
t : Set β
⊢ ∀ (x : γ), x ∈ image2 f ∅ t ↔ x ∈ ∅

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Disjoint.lean
theorem Codisjoint.ne (ha : a ≠ ⊤) (hab : Codisjoint a b) : a ≠ b :=
  fun h ↦ ha <| codisjoint_self.1 <| by rwa [← h] at hab

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
a b : α
ha : a ≠ ⊤
hab : Codisjoint a b
h : a = b
⊢ Codisjoint a a

Tactic:
rwa [← h] at hab

Result:
no goals
-- Mathlib/Data/Set/MulAntidiagonal.lean
theorem swap_mem_mulAntidiagonal_aux [CommSemigroup α] {s t : Set α} {a : α} {x : α × α} :
    x.snd ∈ s ∧ x.fst ∈ t ∧ x.snd * x.fst = a
      ↔ x ∈ Set.mulAntidiagonal t s a

Proof state:
α : Type u_1
inst✝ : CommSemigroup α
s t : Set α
a : α
x : α × α
⊢ x.2 ∈ s ∧ x.1 ∈ t ∧ x.2 * x.1 = a ↔ x ∈ t.mulAntidiagonal s a

Tactic:
simp [mul_comm, and_left_comm]

Result:
no goals
-- Mathlib/Data/Finset/Pi.lean
@[simp]
lemma pi_nonempty : (s.pi t).Nonempty ↔ ∀ a ∈ s, (t a).Nonempty

Proof state:
α : Type u_1
β : α → Type u
s : Finset α
t : (a : α) → Finset (β a)
inst✝ : DecidableEq α
⊢ (s.pi t).Nonempty ↔ ∀ a ∈ s, (t a).Nonempty

Tactic:
simp [Finset.Nonempty, Classical.skolem]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem min_self_assoc' {m n : Nat} : min n (min m n) = min n m

Proof state:
m n : Nat
⊢ min n (min m n) = min n m

Tactic:
rw [Nat.min_comm m n, ← Nat.min_assoc, Nat.min_self]

Result:
no goals
-- Mathlib/Data/Nat/GCD/Basic.lean
theorem coprime_self_sub_left {m n : ℕ} (h : m ≤ n) : Coprime (n - m) n ↔ Coprime m n

Proof state:
m n : ℕ
h : m ≤ n
⊢ (n - m).Coprime n ↔ m.Coprime n

Tactic:
rw [Coprime, Coprime, gcd_self_sub_left h]

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Basic.lean
theorem simple_mul_simple_cancel_left {w : W} (i : B) : s i * (s i * w) = w

Proof state:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.simple i * (cs.simple i * w) = w

Tactic:
simp [← mul_assoc]

Result:
no goals
-- Mathlib/Data/Finset/Card.lean
theorem fiber_card_ne_zero_iff_mem_image (s : Finset α) (f : α → β) [DecidableEq β] (y : β) :
    #(s.filter fun x ↦ f x = y) ≠ 0 ↔ y ∈ s.image f

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst✝ : DecidableEq β
y : β
⊢ #(filter (fun x => f x = y) s) ≠ 0 ↔ y ∈ image f s

Tactic:
rw [← Nat.pos_iff_ne_zero, card_pos, fiber_nonempty_iff_mem_image]

Result:
no goals
-- Mathlib/Deprecated/Cardinal/PartENat.lean
theorem mk_toPartENat_eq_coe_card [Fintype α] : toPartENat #α = Fintype.card α

Proof state:
α : Type u
inst✝ : Fintype α
⊢ toPartENat #α = ↑(Fintype.card α)

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Basic.lean
theorem mem_restrict' : J₁ ∈ π.restrict J ↔ ∃ J' ∈ π, (J₁ : Set (ι → ℝ)) = ↑J ∩ ↑J'

Proof state:
ι : Type u_1
I J J₁ : Box ι
π : Prepartition I
⊢ J₁ ∈ π.restrict J ↔ ∃ J' ∈ π, ↑J₁ = ↑J ∩ ↑J'

Tactic:
simp only [mem_restrict, ← Box.withBotCoe_inj, Box.coe_inf, Box.coe_coe]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
theorem _root_.Sbtw.oangle_sign_eq {p₁ p₂ p₃ : P} (p₄ : P) (h : Sbtw ℝ p₁ p₂ p₃) :
    (∡ p₁ p₄ p₂).sign = (∡ p₂ p₄ p₃).sign :=
  haveI hc : Collinear ℝ ({p₁, p₂, p₂, p₃} : Set P)

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : Sbtw ℝ p₁ p₂ p₃
⊢ Collinear ℝ {p₁, p₂, p₂, p₃}

Tactic:
simpa using h.wbtw.collinear

Result:
no goals
-- Mathlib/Order/SuccPred/InitialSeg.lean
theorem apply_wCovBy_apply_iff (f : α ≤i β) : f a ⩿ f b ↔ a ⩿ b

Proof state:
α : Type u_1
β : Type u_2
a b : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
⊢ f a ⩿ f b ↔ a ⩿ b

Tactic:
simp [wcovBy_iff_eq_or_covBy]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Limits.lean
theorem preserves_lift_mapCone (c₁ c₂ : Cone F) (t : IsLimit c₁) :
    (isLimitOfPreserves G t).lift (G.mapCone c₂) = G.map (t.lift c₂) :=
  ((isLimitOfPreserves G t).uniq (G.mapCone c₂) _ (by simp [← G.map_comp])).symm

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝¹ : Category.{w', w} J
F : J ⥤ C
inst✝ : PreservesLimit F G
c₁ c₂ : Cone F
t : IsLimit c₁
⊢ ∀ (j : J), G.map (t.lift c₂) ≫ (G.mapCone c₁).π.app j = (G.mapCone c₂).π.app j

Tactic:
simp [← G.map_comp]

Result:
no goals
-- Mathlib/Analysis/SpecificLimits/Basic.lean
theorem le_geom {u : ℕ → ℝ} {c : ℝ} (hc : 0 ≤ c) (n : ℕ) (h : ∀ k < n, u (k + 1) ≤ c * u k) :
    u n ≤ c ^ n * u 0

Proof state:
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
h : ∀ k < n, u (k + 1) ≤ c * u k
⊢ u n ≤ c ^ n * u 0

Tactic:
apply (monotone_mul_left_of_nonneg hc).seq_le_seq n _ h _ <;>
  simp [_root_.pow_succ', mul_assoc, le_refl]

Result:
no goals
-- Mathlib/Data/List/Cycle.lean
theorem toFinset_eq_nil {s : Cycle α} : s.toFinset = ∅ ↔ s = Cycle.nil :=
  Quotient.inductionOn' s (by simp)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
⊢ ∀ (a : List α), toFinset (Quotient.mk'' a) = ∅ ↔ Quotient.mk'' a = nil

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean
theorem rotation_neg_orientation_eq_neg (θ : Real.Angle) : (-o).rotation θ = o.rotation (-θ) :=
  LinearIsometryEquiv.ext <| by simp [rotation_apply]

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
⊢ ∀ (x : V), ((-o).rotation θ) x = (o.rotation (-θ)) x

Tactic:
simp [rotation_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem mul_ne_zero_iff : n * m ≠ 0 ↔ n ≠ 0 ∧ m ≠ 0

Proof state:
n m : Nat
⊢ n * m ≠ 0 ↔ n ≠ 0 ∧ m ≠ 0

Tactic:
rw [ne_eq, mul_eq_zero, not_or]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem add_eq_self {c : Cardinal} (h : ℵ₀ ≤ c) : c + c = c :=
  le_antisymm
    (by
      convert mul_le_mul_right' ((nat_lt_aleph0 2).le.trans h) c using 1
      <;> simp [two_mul, mul_eq_self h])
    (self_le_add_left c c)

Proof state:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c + c ≤ c

Tactic:
convert mul_le_mul_right' ((nat_lt_aleph0 2).le.trans h) c using 1
<;> simp [two_mul, mul_eq_self h]

Result:
no goals
-- Mathlib/Probability/Independence/Kernel.lean
@[simp] lemma indep_zero_right {m₁ m₂ : MeasurableSpace Ω} {_mΩ : MeasurableSpace Ω}
    {κ : Kernel α Ω} : Indep m₁ m₂ κ 0

Proof state:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ _mΩ : MeasurableSpace Ω
κ : Kernel α Ω
⊢ Indep m₁ m₂ κ 0

Tactic:
simp [Indep]

Result:
no goals
-- Mathlib/Computability/Ackermann.lean
theorem ack_succ_succ (m n : ℕ) : ack (m + 1) (n + 1) = ack m (ack (m + 1) n)

Proof state:
m n : ℕ
⊢ ack (m + 1) (n + 1) = ack m (ack (m + 1) n)

Tactic:
rw [ack]

Result:
no goals
-- Mathlib/CategoryTheory/Localization/CalculusOfFractions/Preadditive.lean
lemma add_eq (f₁ f₂ : X' ⟶ Y') :
    letI := addCommGroup L W X' Y'
    f₁ + f₂ = add W eX eY f₁ f₂

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
X' Y' : D
eX : L.obj X ≅ X'
eY : L.obj Y ≅ Y'
f₁ f₂ : X' ⟶ Y'
⊢ f₁ + f₂ = add W eX eY f₁ f₂

Tactic:
apply add_eq_add

Result:
no goals
-- Mathlib/Order/Sublattice.lean
lemma map_top (f : LatticeHom α β) (h : Surjective f) : Sublattice.map f ⊤ = ⊤ :=
  SetLike.coe_injective <| by simp [h.range_eq]

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
f : LatticeHom α β
h : Surjective ⇑f
⊢ ↑(map f ⊤) = ↑⊤

Tactic:
simp [h.range_eq]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean
theorem tan_arccos (x : ℝ) : tan (arccos x) = √(1 - x ^ 2) / x

Proof state:
x : ℝ
⊢ tan (arccos x) = √(1 - x ^ 2) / x

Tactic:
rw [arccos, tan_pi_div_two_sub, tan_arcsin, inv_div]

Result:
no goals
-- Mathlib/CategoryTheory/Linear/Basic.lean
@[simp]
lemma units_smul_comp {X Y Z : C} (r : Rˣ) (f : X ⟶ Y) (g : Y ⟶ Z) :
    (r • f) ≫ g = r • f ≫ g

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type w
inst✝¹ : Semiring R
inst✝ : Linear R C
X Y Z : C
r : Rˣ
f : X ⟶ Y
g : Y ⟶ Z
⊢ (r • f) ≫ g = r • f ≫ g

Tactic:
apply Linear.smul_comp

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem image_mul_left_Icc {a b c : α} (ha : 0 ≤ a) (hbc : b ≤ c) :
    (a * ·) '' Icc b c = Icc (a * b) (a * c)

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a b c : α
ha : 0 ≤ a
hbc : b ≤ c
⊢ (fun x => a * x) '' Icc b c = Icc (a * b) (a * c)

Tactic:
convert image_mul_right_Icc hbc ha using 1 <;> simp only [mul_comm _ a]

Result:
no goals
-- Mathlib/Geometry/Manifold/Algebra/LeftInvariantDerivation.lean
theorem map_add : X (f + f') = X f + X f'

Proof state:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Monoid G
inst✝ : ContMDiffMul I ∞ G
X : LeftInvariantDerivation I G
f f' : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
⊢ X (f + f') = X f + X f'

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Ico_subset_Icc_self : Ico a b ⊆ Icc a b

Proof state:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Set.Ico a b ⊆ Set.Icc a b

Tactic:
exact Set.Ico_subset_Icc_self

Result:
no goals

Proof state:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Ico a b ⊆ Icc a b

Tactic:
rw [← coe_subset, coe_Ico, coe_Icc]

Result:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Set.Ico a b ⊆ Set.Icc a b
-- Mathlib/Combinatorics/Additive/CauchyDavenport.lean
@[to_additive]
private lemma devosMulRel_iff :
    DevosMulRel x y ↔
      #(x.1 * x.2) < #(y.1 * y.2) ∨
        #(x.1 * x.2) = #(y.1 * y.2) ∧ #y.1 + #y.2 < #x.1 + #x.2 ∨
          #(x.1 * x.2) = #(y.1 * y.2) ∧ #x.1 + #x.2 = #y.1 + #y.2 ∧ #x.1 < #y.1

Proof state:
α : Type u_1
inst✝¹ : Group α
inst✝ : DecidableEq α
x y : Finset α × Finset α
⊢ DevosMulRel x y ↔
    #(x.1 * x.2) < #(y.1 * y.2) ∨
      #(x.1 * x.2) = #(y.1 * y.2) ∧ #y.1 + #y.2 < #x.1 + #x.2 ∨
        #(x.1 * x.2) = #(y.1 * y.2) ∧ #x.1 + #x.2 = #y.1 + #y.2 ∧ #x.1 < #y.1

Tactic:
simp [DevosMulRel, Prod.lex_iff, and_or_left]

Result:
no goals
-- Mathlib/Topology/Order/Bornology.lean
@[simp] lemma orderBornology_isBounded : orderBornology.IsBounded s ↔ BddBelow s ∧ BddAbove s

Proof state:
α : Type u_1
s : Set α
inst✝¹ : Lattice α
inst✝ : Nonempty α
⊢ IsBounded s ↔ BddBelow s ∧ BddAbove s

Tactic:
simp [IsBounded, IsCobounded, -isCobounded_compl_iff]

Result:
no goals
-- Mathlib/Topology/Homeomorph.lean
theorem map_cocompact (h : X ≃ₜ Y) : map h (cocompact X) = cocompact Y

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
⊢ map (⇑h) (cocompact X) = cocompact Y

Tactic:
rw [← h.comap_cocompact, map_comap_of_surjective h.surjective]

Result:
no goals
-- Mathlib/CategoryTheory/Subpresheaf/Image.lean
lemma epi_iff_range_eq_top :
    Epi p ↔ range p = ⊤

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F F' : Cᵒᵖ ⥤ Type w
p : F' ⟶ F
⊢ Epi p ↔ range p = ⊤

Tactic:
simp [NatTrans.epi_iff_epi_app, epi_iff_surjective, Subpresheaf.ext_iff, funext_iff,
  Set.range_eq_univ]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/l2Space.lean
theorem linearIsometry_apply_dfinsupp_sum_single [DecidableEq ι] [∀ i, DecidableEq (G i)]
    (W₀ : Π₀ i : ι, G i) : hV.linearIsometry (W₀.sum (lp.single 2)) = W₀.sum fun i => V i

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝⁷ : RCLike 𝕜
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝⁴ : (i : ι) → NormedAddCommGroup (G i)
inst✝³ : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝² : CompleteSpace E
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
W₀ : Π₀ (i : ι), G i
⊢ hV.linearIsometry (W₀.sum (lp.single 2)) = W₀.sum fun i => ⇑(V i)

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean
theorem IsEquivalent.tendsto_atBot [OrderTopology β] (huv : u ~[l] v) (hu : Tendsto u l atBot) :
    Tendsto v l atBot

Proof state:
case h.e'_3.h
α : Type u_1
β : Type u_2
inst✝¹ : NormedLinearOrderedField β
u v : α → β
l : Filter α
inst✝ : OrderTopology β
huv : u ~[l] v
hu : Tendsto u l atBot
x✝ : α
⊢ v x✝ = (Neg.neg ∘ fun x => -v x) x✝

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_3
α : Type u_1
β : Type u_2
inst✝¹ : NormedLinearOrderedField β
u v : α → β
l : Filter α
inst✝ : OrderTopology β
huv : u ~[l] v
hu : Tendsto u l atBot
⊢ v = Neg.neg ∘ fun x => -v x

Tactic:
ext

Result:
case h.e'_3.h
α : Type u_1
β : Type u_2
inst✝¹ : NormedLinearOrderedField β
u v : α → β
l : Filter α
inst✝ : OrderTopology β
huv : u ~[l] v
hu : Tendsto u l atBot
x✝ : α
⊢ v x✝ = (Neg.neg ∘ fun x => -v x) x✝

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : NormedLinearOrderedField β
u v : α → β
l : Filter α
inst✝ : OrderTopology β
huv : u ~[l] v
hu : Tendsto u l atBot
⊢ Tendsto v l atBot

Tactic:
convert tendsto_neg_atTop_atBot.comp (huv.neg.tendsto_atTop <| tendsto_neg_atBot_atTop.comp hu)

Result:
case h.e'_3
α : Type u_1
β : Type u_2
inst✝¹ : NormedLinearOrderedField β
u v : α → β
l : Filter α
inst✝ : OrderTopology β
huv : u ~[l] v
hu : Tendsto u l atBot
⊢ v = Neg.neg ∘ fun x => -v x
-- Mathlib/Algebra/Algebra/Basic.lean
theorem map_algebraMap_mul (f : A →ₗ[R] B) (a : A) (r : R) :
    f (algebraMap R A r * a) = algebraMap R B r * f a

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₗ[R] B
a : A
r : R
⊢ f ((algebraMap R A) r * a) = (algebraMap R B) r * f a

Tactic:
rw [← Algebra.smul_def, ← Algebra.smul_def, map_smul]

Result:
no goals
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem lift_eq_iff {x y : M × S} :
    f.lift hg (f.mk' x.1 x.2) = f.lift hg (f.mk' y.1 y.2) ↔ g (x.1 * y.2) = g (y.1 * x.2)

Proof state:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
x y : M × ↥S
⊢ (f.lift hg) (f.mk' x.1 x.2) = (f.lift hg) (f.mk' y.1 y.2) ↔ g (x.1 * ↑y.2) = g (y.1 * ↑x.2)

Tactic:
rw [lift_mk', lift_mk', mul_inv hg]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem monomial_eq_monomial_iff {m n : ℕ} {a b : R} :
    monomial m a = monomial n b ↔ m = n ∧ a = b ∨ a = 0 ∧ b = 0

Proof state:
R : Type u
inst✝ : Semiring R
m n : ℕ
a b : R
⊢ (monomial m) a = (monomial n) b ↔ m = n ∧ a = b ∨ a = 0 ∧ b = 0

Tactic:
rw [← toFinsupp_inj, toFinsupp_monomial, toFinsupp_monomial, Finsupp.single_eq_single_iff]

Result:
no goals
-- Mathlib/RingTheory/PowerBasis.lean
theorem degree_minpoly [Nontrivial A] (pb : PowerBasis A S) :
    degree (minpoly A pb.gen) = pb.dim

Proof state:
S : Type u_2
inst✝³ : Ring S
A : Type u_4
inst✝² : CommRing A
inst✝¹ : Algebra A S
inst✝ : Nontrivial A
pb : PowerBasis A S
⊢ (minpoly A pb.gen).degree = ↑pb.dim

Tactic:
rw [← minpolyGen_eq, degree_minpolyGen]

Result:
no goals
-- Mathlib/Algebra/Algebra/Subalgebra/Directed.lean
theorem iSupLift_comp_inclusion {dir : Directed (· ≤ ·) K} {f : ∀ i, K i →ₐ[R] B}
    {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)}
    {T : Subalgebra R A} {hT : T = iSup K} {i : ι} (h : K i ≤ T) :
    (iSupLift K dir f hf T hT).comp (inclusion h) = f i

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun x1 x2 => x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T = iSup K
i : ι
h : K i ≤ T
⊢ (iSupLift K dir f hf T hT).comp (inclusion h) = f i

Tactic:
ext

Result:
case H
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun x1 x2 => x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T = iSup K
i : ι
h : K i ≤ T
x✝ : ↥(K i)
⊢ ((iSupLift K dir f hf T hT).comp (inclusion h)) x✝ = (f i) x✝

Proof state:
case H
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun x1 x2 => x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T = iSup K
i : ι
h : K i ≤ T
x✝ : ↥(K i)
⊢ ((iSupLift K dir f hf T hT).comp (inclusion h)) x✝ = (f i) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/Data/List/ReduceOption.lean
theorem reduceOption_cons_of_some (x : α) (l : List (Option α)) :
    reduceOption (some x :: l) = x :: l.reduceOption

Proof state:
α : Type u_1
x : α
l : List (Option α)
⊢ (some x :: l).reduceOption = x :: l.reduceOption

Tactic:
simp only [reduceOption, filterMap, id, eq_self_iff_true, and_self_iff]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_zero_pos (x : ℝ) : 0 < x ^ (0 : ℝ)

Proof state:
x : ℝ
⊢ 0 < x ^ 0

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Analytic/CPolynomial.lean
theorem HasFiniteFPowerSeriesOnBall.neg (hf : HasFiniteFPowerSeriesOnBall f pf x n r) :
    HasFiniteFPowerSeriesOnBall (-f) (-pf) x n r :=
  ⟨hf.1.neg, fun m hm ↦ by rw [Pi.neg_apply, hf.finite m hm, neg_zero]⟩

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
pf : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
n : ℕ
hf : HasFiniteFPowerSeriesOnBall f pf x n r
m : ℕ
hm : n ≤ m
⊢ (-pf) m = 0

Tactic:
rw [Pi.neg_apply, hf.finite m hm, neg_zero]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
theorem mult_isReal (w : {w : InfinitePlace K // IsReal w}) :
    mult w.1 = 1

Proof state:
K : Type u_2
inst✝ : Field K
w : { w // w.IsReal }
⊢ (↑w).mult = 1

Tactic:
rw [mult, if_pos w.prop]

Result:
no goals
-- Mathlib/CategoryTheory/ChosenFiniteProducts/FunctorCategory.lean
@[reassoc (attr := simp)]
lemma whiskerRight_app_snd {F₁ F₁' : J ⥤ C} (f : F₁ ⟶ F₁') (F₂ : J ⥤ C) (j : J) :
    (f ▷ F₂).app j ≫ snd _ _ = snd _ _ :=
  (tensorHom_app_snd f (𝟙 F₂) j).trans (by simp)

Proof state:
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
inst✝ : ChosenFiniteProducts C
F₁ F₁' : J ⥤ C
f : F₁ ⟶ F₁'
F₂ : J ⥤ C
j : J
⊢ snd (F₁.obj j) (F₂.obj j) ≫ (𝟙 F₂).app j = snd (F₁.obj j) (F₂.obj j)

Tactic:
simp

Result:
no goals
-- Mathlib/FieldTheory/Relrank.lean
theorem inf_relrank_left : relrank (A ⊓ B) A = relrank B A

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B : IntermediateField F E
⊢ (A ⊓ B).relrank A = B.relrank A

Tactic:
rw [inf_comm, inf_relrank_right]

Result:
no goals
-- Mathlib/LinearAlgebra/Finsupp/Supported.lean
theorem supported_union (s t : Set α) :
    supported M R (s ∪ t) = supported M R s ⊔ supported M R t

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
⊢ supported M R (s ∪ t) = supported M R s ⊔ supported M R t

Tactic:
rw [Set.union_eq_iUnion, supported_iUnion, iSup_bool_eq, cond_true, cond_false]

Result:
no goals
-- Mathlib/Algebra/Order/Hom/Ring.lean
theorem cancel_left {f : β →+*o γ} {g₁ g₂ : α →+*o β} (hf : Injective f) :
    f.comp g₁ = f.comp g₂ ↔ g₁ = g₂ :=
  ⟨fun h => ext fun a => hf <| by rw [← comp_apply, h, comp_apply], congr_arg _⟩

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : NonAssocSemiring α
inst✝⁴ : Preorder α
inst✝³ : NonAssocSemiring β
inst✝² : Preorder β
inst✝¹ : NonAssocSemiring γ
inst✝ : Preorder γ
f : β →+*o γ
g₁ g₂ : α →+*o β
hf : Injective ⇑f
h : f.comp g₁ = f.comp g₂
a : α
⊢ f (g₁ a) = f (g₂ a)

Tactic:
rw [← comp_apply, h, comp_apply]

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem range_toPullbackDiag (f : X → Y) : range (toPullbackDiag f) = pullbackDiagonal f

Proof state:
X : Type u_1
Y : Sort u_2
f : X → Y
⊢ range (toPullbackDiag f) = pullbackDiagonal f

Tactic:
rw [← image_univ, image_toPullbackDiag, univ_prod_univ, preimage_univ, inter_univ]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/FundThmCalculus.lean
theorem integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_right
    (hab : IntervalIntegrable f volume a b) (hmeas : StronglyMeasurableAtFilter f lb')
    (hf : Tendsto f (lb' ⊓ ae volume) (𝓝 c)) (hu : Tendsto u lt lb) (hv : Tendsto v lt lb) :
    (fun t => ((∫ x in a..v t, f x) - ∫ x in a..u t, f x) - (v t - u t) • c) =o[lt] (v - u)

Proof state:
ι : Type u_1
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : ℝ → E
c : E
lb lb' : Filter ℝ
lt : Filter ι
a b : ℝ
u v : ι → ℝ
inst✝ : FTCFilter b lb lb'
hab : IntervalIntegrable f volume a b
hmeas : StronglyMeasurableAtFilter f lb' volume
hf : Tendsto f (lb' ⊓ ae volume) (𝓝 c)
hu : Tendsto u lt lb
hv : Tendsto v lt lb
⊢ (fun t => ((∫ (x : ℝ) in a..v t, f x) - ∫ (x : ℝ) in a..u t, f x) - (v t - u t) • c) =o[lt] (v - u)

Tactic:
simpa only [integral_const, smul_eq_mul, mul_one] using
  measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_right hab hmeas hf hu hv

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Cardinal.lean
theorem cardinalMk_le_max : #(MvPolynomial σ R) ≤ max (max #R #σ) ℵ₀ :=
  cardinalMk_le_max_lift.trans <| by rw [lift_id, lift_id]

Proof state:
σ R : Type u
inst✝ : CommSemiring R
⊢ lift.{u, u} #R ⊔ lift.{u, u} #σ ⊔ ℵ₀ ≤ #R ⊔ #σ ⊔ ℵ₀

Tactic:
rw [lift_id, lift_id]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Hom.lean
theorem zero : (0 : NormedAddGroupHom V₁ V₂).NormNoninc := fun v => by simp

Proof state:
V₁ : Type u_3
V₂ : Type u_4
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
v : V₁
⊢ ‖0 v‖ ≤ ‖v‖

Tactic:
simp

Result:
no goals