harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Polynomial/Content.lean
theorem isPrimitive_iff_content_eq_one {p : R[X]} : p.IsPrimitive ↔ p.content = 1

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ p.IsPrimitive ↔ p.content = 1

Tactic:
rw [← normalize_content, normalize_eq_one, IsPrimitive]

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ (∀ (r : R), C r ∣ p → IsUnit r) ↔ IsUnit p.content

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ (∀ (r : R), r ∣ p.content → IsUnit r) ↔ IsUnit p.content

Tactic:
exact ⟨fun h => h p.content (dvd_refl p.content), fun h r hdvd => isUnit_of_dvd_unit hdvd h⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ (∀ (r : R), C r ∣ p → IsUnit r) ↔ IsUnit p.content

Tactic:
simp_rw [← dvd_content_iff_C_dvd]

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ (∀ (r : R), r ∣ p.content → IsUnit r) ↔ IsUnit p.content
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem add_mk_eq_self {α : Type*} [Infinite α] : #α + #α = #α

Proof state:
α : Type u_1
inst✝ : Infinite α
⊢ #α + #α = #α

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicIntegers.lean
theorem mk_coe (k : ℤ_[p]) : (⟨k, k.2⟩ : ℤ_[p]) = k

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ_[p]
⊢ ⟨↑k, ⋯⟩ = k

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Compactness/Lindelof.lean
theorem IsLindelof.disjoint_nhdsSet_right {l : Filter X} [CountableInterFilter l]
    (hs : IsLindelof s) : Disjoint l (𝓝ˢ s) ↔ ∀ x ∈ s, Disjoint l (𝓝 x)

Proof state:
X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
l : Filter X
inst✝ : CountableInterFilter l
hs : IsLindelof s
⊢ Disjoint l (𝓝ˢ s) ↔ ∀ x ∈ s, Disjoint l (𝓝 x)

Tactic:
simpa only [disjoint_comm] using hs.disjoint_nhdsSet_left

Result:
no goals
-- Mathlib/RingTheory/Localization/Away/Basic.lean
lemma surj (z : S) : ∃ (n : ℕ) (a : R), z * algebraMap R S x ^ n = algebraMap R S a

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : Away x S
z : S
⊢ ∃ n a, z * (algebraMap R S) x ^ n = (algebraMap R S) a

Tactic:
obtain ⟨⟨a, ⟨-, n, rfl⟩⟩, h⟩ := IsLocalization.surj (Submonoid.powers x) z

Result:
case intro.mk.mk.intro
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : Away x S
z : S
a : R
n : ℕ
h : z * (algebraMap R S) ↑(a, ⟨(fun x_1 => x ^ x_1) n, ⋯⟩).2 = (algebraMap R S) (a, ⟨(fun x_1 => x ^ x_1) n, ⋯⟩).1
⊢ ∃ n a, z * (algebraMap R S) x ^ n = (algebraMap R S) a

Proof state:
case intro.mk.mk.intro
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : Away x S
z : S
a : R
n : ℕ
h : z * (algebraMap R S) ↑(a, ⟨(fun x_1 => x ^ x_1) n, ⋯⟩).2 = (algebraMap R S) (a, ⟨(fun x_1 => x ^ x_1) n, ⋯⟩).1
⊢ ∃ n a, z * (algebraMap R S) x ^ n = (algebraMap R S) a

Tactic:
use n, a

Result:
case h
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : Away x S
z : S
a : R
n : ℕ
h : z * (algebraMap R S) ↑(a, ⟨(fun x_1 => x ^ x_1) n, ⋯⟩).2 = (algebraMap R S) (a, ⟨(fun x_1 => x ^ x_1) n, ⋯⟩).1
⊢ z * (algebraMap R S) x ^ n = (algebraMap R S) a

Proof state:
case h
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : Away x S
z : S
a : R
n : ℕ
h : z * (algebraMap R S) ↑(a, ⟨(fun x_1 => x ^ x_1) n, ⋯⟩).2 = (algebraMap R S) (a, ⟨(fun x_1 => x ^ x_1) n, ⋯⟩).1
⊢ z * (algebraMap R S) x ^ n = (algebraMap R S) a

Tactic:
simpa using h

Result:
no goals
-- Mathlib/CategoryTheory/LiftingProperties/Adjunction.lean
theorem left_adjoint (sq : CommSq u i (F.map p) v) (adj : G ⊣ F) :
    CommSq ((adj.homEquiv _ _).symm u) (G.map i) p ((adj.homEquiv _ _).symm v) :=
  ⟨by
    simp only [Adjunction.homEquiv_counit, assoc, ← G.map_comp_assoc, ← sq.w]
    rw [G.map_comp, assoc, Adjunction.counit_naturality]⟩

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : A ⟶ F.obj X
v : B ⟶ F.obj Y
sq : CommSq u i (F.map p) v
adj : G ⊣ F
⊢ G.map u ≫ adj.counit.app X ≫ p = G.map (u ≫ F.map p) ≫ adj.counit.app Y

Tactic:
rw [G.map_comp, assoc, Adjunction.counit_naturality]

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : A ⟶ F.obj X
v : B ⟶ F.obj Y
sq : CommSq u i (F.map p) v
adj : G ⊣ F
⊢ (adj.homEquiv A X).symm u ≫ p = G.map i ≫ (adj.homEquiv B Y).symm v

Tactic:
simp only [Adjunction.homEquiv_counit, assoc, ← G.map_comp_assoc, ← sq.w]

Result:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : A ⟶ F.obj X
v : B ⟶ F.obj Y
sq : CommSq u i (F.map p) v
adj : G ⊣ F
⊢ G.map u ≫ adj.counit.app X ≫ p = G.map (u ≫ F.map p) ≫ adj.counit.app Y
-- Mathlib/RingTheory/Finiteness/Basic.lean
theorem of_surjective [hM : Module.Finite R M] (f : M →ₛₗ[σ] P) (hf : Surjective f) :
    Module.Finite S P :=
  ⟨by
    rw [← LinearMap.range_eq_top.2 hf, ← Submodule.map_top]
    exact hM.1.map f⟩

Proof state:
R : Type u_1
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_7
P : Type u_6
inst✝³ : Semiring S
inst✝² : AddCommMonoid P
inst✝¹ : Module S P
σ : R →+* S
inst✝ : RingHomSurjective σ
hM : Module.Finite R M
f : M →ₛₗ[σ] P
hf : Surjective ⇑f
⊢ (map f ⊤).FG

Tactic:
exact hM.1.map f

Result:
no goals

Proof state:
R : Type u_1
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_7
P : Type u_6
inst✝³ : Semiring S
inst✝² : AddCommMonoid P
inst✝¹ : Module S P
σ : R →+* S
inst✝ : RingHomSurjective σ
hM : Module.Finite R M
f : M →ₛₗ[σ] P
hf : Surjective ⇑f
⊢ ⊤.FG

Tactic:
rw [← LinearMap.range_eq_top.2 hf, ← Submodule.map_top]

Result:
R : Type u_1
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_7
P : Type u_6
inst✝³ : Semiring S
inst✝² : AddCommMonoid P
inst✝¹ : Module S P
σ : R →+* S
inst✝ : RingHomSurjective σ
hM : Module.Finite R M
f : M →ₛₗ[σ] P
hf : Surjective ⇑f
⊢ (map f ⊤).FG
-- Mathlib/Algebra/Homology/TotalComplexSymmetry.lean
@[reassoc]
lemma totalFlipIso_hom_f_D₁ (j j' : J) :
    (K.totalFlipIso c).hom.f j ≫ K.D₁ c j j' =
      K.flip.D₂ c j j' ≫ (K.totalFlipIso c).hom.f j'

Proof state:
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁶ : Category.{u_5, u_1} C
inst✝⁵ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c
inst✝³ : TotalComplexShape c₂ c₁ c
inst✝² : TotalComplexShapeSymmetry c₁ c₂ c
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
j j' : J
⊢ (K.totalFlipIso c).hom.f j ≫ K.D₁ c j j' = K.flip.D₂ c j j' ≫ (K.totalFlipIso c).hom.f j'

Tactic:
apply totalFlipIsoX_hom_D₁

Result:
no goals
-- Mathlib/CategoryTheory/GradedObject.lean
@[reassoc (attr := simp)]
lemma map_inv_hom_id_eval_app (e : X ≅ Y) (F : C ⥤ D ⥤ E) (j : J) (Y : D) :
    (F.map (e.inv j)).app Y ≫ (F.map (e.hom j)).app Y = 𝟙 _

Proof state:
C : Type u_1
D : Type u_2
E : Type u_3
J : Type u_4
inst✝² : Category.{u_5, u_1} C
inst✝¹ : Category.{u_7, u_2} D
inst✝ : Category.{u_6, u_3} E
X Y✝ : GradedObject J C
e : X ≅ Y✝
F : C ⥤ D ⥤ E
j : J
Y : D
⊢ (F.map (e.inv j)).app Y ≫ (F.map (e.hom j)).app Y = 𝟙 ((F.obj (Y✝ j)).obj Y)

Tactic:
rw [← NatTrans.comp_app, ← F.map_comp, inv_hom_id_eval,
  Functor.map_id, NatTrans.id_app]

Result:
no goals
-- Mathlib/Data/ZMod/ValMinAbs.lean
lemma valMinAbs_def_pos : ∀ {n : ℕ} [NeZero n] (x : ZMod n),
    valMinAbs x = if x.val ≤ n / 2 then (x.val : ℤ) else x.val - n
  | 0, _, x => by cases NeZero.ne 0 rfl
  | n + 1, _, x => rfl

Proof state:
x✝ : NeZero 0
x : ZMod 0
⊢ x.valMinAbs = if x.val ≤ 0 / 2 then ↑x.val else ↑x.val - ↑0

Tactic:
cases NeZero.ne 0 rfl

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
@[to_additive (attr := simp)]
lemma dens_smul_finset [Fintype β] (a : α) (s : Finset β) : (a • s).dens = s.dens

Proof state:
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq β
inst✝² : Group α
inst✝¹ : MulAction α β
inst✝ : Fintype β
a : α
s : Finset β
⊢ (a • s).dens = s.dens

Tactic:
simp [dens]

Result:
no goals
-- Mathlib/Data/Nat/Bitwise.lean
theorem bit_ne_zero_iff {n : ℕ} {b : Bool} : n.bit b ≠ 0 ↔ n = 0 → b = true

Proof state:
n : ℕ
b : Bool
⊢ bit b n ≠ 0 ↔ n = 0 → b = true

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Analytic/OfScalars.lean
theorem tendsto_succ_norm_div_norm {r r' : ℝ≥0} (hr' : r' ≠ 0)
    (hc : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 r)) :
      Tendsto (fun n ↦ ‖‖c (n + 1)‖ * r' ^ (n + 1)‖ /
        ‖‖c n‖ * r' ^ n‖) atTop (𝓝 ↑(r' * r))

Proof state:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
c : ℕ → 𝕜
r r' : ℝ≥0
hr' : r' ≠ 0
hc : Tendsto (fun n => ‖c n.succ‖ / ‖c n‖) atTop (𝓝 ↑r)
⊢ Tendsto (fun n => ‖‖c (n + 1)‖ * ↑r' ^ (n + 1)‖ / ‖‖c n‖ * ↑r' ^ n‖) atTop (𝓝 ↑(r' * r))

Tactic:
simp_rw [norm_mul, norm_norm, mul_div_mul_comm, ← norm_div, pow_succ, mul_div_right_comm,
  div_self (pow_ne_zero _ (NNReal.coe_ne_zero.mpr hr')), one_mul, norm_div, NNReal.norm_eq]

Result:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
c : ℕ → 𝕜
r r' : ℝ≥0
hr' : r' ≠ 0
hc : Tendsto (fun n => ‖c n.succ‖ / ‖c n‖) atTop (𝓝 ↑r)
⊢ Tendsto (fun n => ‖c (n + 1)‖ / ‖c n‖ * ↑r') atTop (𝓝 ↑(r' * r))

Proof state:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
c : ℕ → 𝕜
r r' : ℝ≥0
hr' : r' ≠ 0
hc : Tendsto (fun n => ‖c n.succ‖ / ‖c n‖) atTop (𝓝 ↑r)
⊢ Tendsto (fun n => ‖c (n + 1)‖ / ‖c n‖ * ↑r') atTop (𝓝 ↑(r' * r))

Tactic:
exact mul_comm r' r ▸ hc.mul tendsto_const_nhds

Result:
no goals
-- Mathlib/Topology/UniformSpace/Separation.lean
theorem t0Space_iff_ker_uniformity : T0Space α ↔ (𝓤 α).ker = diagonal α

Proof state:
α : Type u
inst✝ : UniformSpace α
⊢ (∀ (a b : α), (∀ s ∈ 𝓤 α, (a, b) ∈ s) → a = b) → ∀ (x : α), ∀ s ∈ 𝓤 α, (x, x) ∈ s

Tactic:
exact fun _ x s hs ↦ refl_mem_uniformity hs

Result:
no goals

Proof state:
α : Type u
inst✝ : UniformSpace α
⊢ T0Space α ↔ (𝓤 α).ker = diagonal α

Tactic:
simp_rw [t0Space_iff_uniformity, subset_antisymm_iff, diagonal_subset_iff, subset_def,
  Prod.forall, Filter.mem_ker, mem_diagonal_iff, iff_self_and]

Result:
α : Type u
inst✝ : UniformSpace α
⊢ (∀ (a b : α), (∀ s ∈ 𝓤 α, (a, b) ∈ s) → a = b) → ∀ (x : α), ∀ s ∈ 𝓤 α, (x, x) ∈ s
-- Mathlib/Order/Filter/Basic.lean
theorem eventuallyLE_antisymm_iff [PartialOrder β] {l : Filter α} {f g : α → β} :
    f =ᶠ[l] g ↔ f ≤ᶠ[l] g ∧ g ≤ᶠ[l] f

Proof state:
α : Type u
β : Type v
inst✝ : PartialOrder β
l : Filter α
f g : α → β
⊢ f =ᶠ[l] g ↔ f ≤ᶠ[l] g ∧ g ≤ᶠ[l] f

Tactic:
simp only [EventuallyEq, EventuallyLE, le_antisymm_iff, eventually_and]

Result:
no goals
-- Mathlib/Order/Filter/CountablyGenerated.lean
theorem exists_antitone_seq (f : Filter α) [f.IsCountablyGenerated] :
    ∃ x : ℕ → Set α, Antitone x ∧ ∀ {s}, s ∈ f ↔ ∃ i, x i ⊆ s :=
  let ⟨x, hx⟩ := f.exists_antitone_basis
  ⟨x, hx.antitone, by simp [hx.1.mem_iff]⟩

Proof state:
α : Type u_1
f : Filter α
inst✝ : f.IsCountablyGenerated
x : ℕ → Set α
hx : f.HasAntitoneBasis x
⊢ ∀ {s : Set α}, s ∈ f ↔ ∃ i, x i ⊆ s

Tactic:
simp [hx.1.mem_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean
theorem toAffineSubspace_direction (s : Submodule k V) : s.toAffineSubspace.direction = s

Proof state:
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Submodule k V
⊢ s.toAffineSubspace.direction = s

Tactic:
ext x

Result:
case h
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Submodule k V
x : V
⊢ x ∈ s.toAffineSubspace.direction ↔ x ∈ s

Proof state:
case h
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Submodule k V
x : V
⊢ x ∈ s.toAffineSubspace.direction ↔ x ∈ s

Tactic:
simp [← s.toAffineSubspace.vadd_mem_iff_mem_direction _ s.zero_mem]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem get?_eq_some_iff : l.get? n = some a ↔ ∃ h, get l ⟨n, h⟩ = a :=
  ⟨fun e =>
    have : n < length l := Nat.gt_of_not_le fun hn => by cases get?_eq_none hn ▸ e
    ⟨this, by rwa [get?_eq_get this, Option.some.injEq] at e⟩,
  fun ⟨_, e⟩ => e ▸ get?_eq_get _⟩

Proof state:
α✝ : Type u_1
a : α✝
l : List α✝
n : Nat
e : l.get? n = some a
this : n < l.length
⊢ l.get ⟨n, this⟩ = a

Tactic:
rwa [get?_eq_get this, Option.some.injEq] at e

Result:
no goals

Proof state:
α✝ : Type u_1
a : α✝
l : List α✝
n : Nat
e : l.get? n = some a
hn : l.length ≤ n
⊢ False

Tactic:
cases get?_eq_none hn ▸ e

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Find.lean
theorem findSome?_eq_none_iff {f : α → Option β} {l : Vector α n} :
    findSome? f l = none ↔ ∀ x ∈ l, f x = none

Proof state:
α : Type u_1
β : Type u_2
n : Nat
f : α → Option β
l : Vector α n
⊢ findSome? f l = none ↔ ∀ (x : α), x ∈ l → f x = none

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
n : Nat
f : α → Option β
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ findSome? f { toArray := toArray✝, size_toArray := size_toArray✝ } = none ↔
    ∀ (x : α), x ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } → f x = none

Proof state:
case mk
α : Type u_1
β : Type u_2
n : Nat
f : α → Option β
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ findSome? f { toArray := toArray✝, size_toArray := size_toArray✝ } = none ↔
    ∀ (x : α), x ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } → f x = none

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem mul_add_mod_self_left (a b c : Nat) : (a * b + c) % a = c % a

Proof state:
a b c : Nat
⊢ (a * b + c) % a = c % a

Tactic:
rw [Nat.add_comm, Nat.add_mul_mod_self_left]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Set/Monoid.lean
theorem Ioc_add_bij : BijOn (· + d) (Ioc a b) (Ioc (a + d) (b + d))

Proof state:
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b d : M
⊢ BijOn (fun x => x + d) (Ioi a ∩ Iic b) (Ioi (a + d) ∩ Iic (b + d))

Tactic:
exact
  (Ioi_add_bij a d).inter_mapsTo (fun x hx => add_le_add_right hx _) fun x hx =>
    le_of_add_le_add_right hx.2

Result:
no goals

Proof state:
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b d : M
⊢ BijOn (fun x => x + d) (Ioc a b) (Ioc (a + d) (b + d))

Tactic:
rw [← Ioi_inter_Iic, ← Ioi_inter_Iic]

Result:
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b d : M
⊢ BijOn (fun x => x + d) (Ioi a ∩ Iic b) (Ioi (a + d) ∩ Iic (b + d))
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
theorem map_top_of_surjective (hf : Function.Surjective f) : AffineSubspace.map f ⊤ = ⊤

Proof state:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
hf : Function.Surjective ⇑f
⊢ ↑(AffineSubspace.map f ⊤) = ↑⊤

Tactic:
exact image_univ_of_surjective hf

Result:
no goals

Proof state:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
hf : Function.Surjective ⇑f
⊢ AffineSubspace.map f ⊤ = ⊤

Tactic:
rw [AffineSubspace.ext_iff]

Result:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
hf : Function.Surjective ⇑f
⊢ ↑(AffineSubspace.map f ⊤) = ↑⊤
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem getThenInsertIfNew?_fst_val [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} {a : α}
    {b : β a} : (m.val.getThenInsertIfNew? a b).1 = (m.getThenInsertIfNew? a b).1

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
a : α
b : β a
⊢ (m.val.getThenInsertIfNew? a b).fst = (m.getThenInsertIfNew? a b).fst

Tactic:
simp [Raw.getThenInsertIfNew?, m.2]

Result:
no goals
-- Mathlib/RingTheory/Localization/NumDen.lean
lemma associated_den_num_inv (x : K) (hx : x ≠ 0) : Associated (den A x : A) (num A x⁻¹) :=
  associated_of_dvd_dvd
    (IsRelPrime.dvd_of_dvd_mul_right (IsFractionRing.num_den_reduced A x).symm <|
      dvd_of_mul_left_dvd (a := (den A x⁻¹ : A)) <| dvd_of_eq <|
      FaithfulSMul.algebraMap_injective A K <| Eq.symm <| eq_of_div_eq_one
      (by simp [mul_div_mul_comm, hx]))
    (IsRelPrime.dvd_of_dvd_mul_right (IsFractionRing.num_den_reduced A x⁻¹) <|
      dvd_of_mul_left_dvd (a := (num A x : A)) <| dvd_of_eq <|
      FaithfulSMul.algebraMap_injective A K <| eq_of_div_eq_one
      (by simp [mul_div_mul_comm, hx]))

Proof state:
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
hx : x ≠ 0
⊢ (algebraMap A K) (num A x⁻¹ * num A x) / (algebraMap A K) (↑(den A x⁻¹) * ↑(den A x)) = 1

Tactic:
simp [mul_div_mul_comm, hx]

Result:
no goals

Proof state:
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
hx : x ≠ 0
⊢ (algebraMap A K) (num A x * num A x⁻¹) / (algebraMap A K) (↑(den A x) * ↑(den A x⁻¹)) = 1

Tactic:
simp [mul_div_mul_comm, hx]

Result:
no goals
-- Mathlib/Topology/Order/IntermediateValue.lean
theorem intermediate_value_uIcc {a b : α} {f : α → δ} (hf : ContinuousOn f [[a, b]]) :
    [[f a, f b]] ⊆ f '' uIcc a b

Proof state:
α : Type u
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a b : α
f : α → δ
hf : ContinuousOn f [[a, b]]
⊢ [[f a, f b]] ⊆ f '' [[a, b]]

Tactic:
cases le_total (f a) (f b) <;> simp [*, isPreconnected_uIcc.intermediate_value]

Result:
no goals
-- Mathlib/Data/Nat/Digits.lean
theorem digits_getLast {b : ℕ} (m : ℕ) (h : 1 < b) (p q) :
    (digits b m).getLast p = (digits b (m / b)).getLast q

Proof state:
case pos
b m : ℕ
h : 1 < b
p : b.digits m ≠ []
q : b.digits (m / b) ≠ []
hm : m = 0
⊢ (b.digits m).getLast p = (b.digits (m / b)).getLast q

Tactic:
simp [hm]

Result:
no goals

Proof state:
b m : ℕ
h : 1 < b
p : b.digits m ≠ []
q : b.digits (m / b) ≠ []
⊢ (b.digits m).getLast p = (b.digits (m / b)).getLast q

Tactic:
by_cases hm : m = 0

Result:
case pos
b m : ℕ
h : 1 < b
p : b.digits m ≠ []
q : b.digits (m / b) ≠ []
hm : m = 0
⊢ (b.digits m).getLast p = (b.digits (m / b)).getLast q

case neg
b m : ℕ
h : 1 < b
p : b.digits m ≠ []
q : b.digits (m / b) ≠ []
hm : ¬m = 0
⊢ (b.digits m).getLast p = (b.digits (m / b)).getLast q

Proof state:
case neg
b m : ℕ
h : 1 < b
p : b.digits m ≠ []
q : b.digits (m / b) ≠ []
hm : ¬m = 0
⊢ (b.digits m).getLast p = (b.digits (m / b)).getLast q

Tactic:
simp only [digits_eq_cons_digits_div h hm]

Result:
case neg
b m : ℕ
h : 1 < b
p : b.digits m ≠ []
q : b.digits (m / b) ≠ []
hm : ¬m = 0
⊢ (m % b :: b.digits (m / b)).getLast ⋯ = (b.digits (m / b)).getLast q

Proof state:
case neg
b m : ℕ
h : 1 < b
p : b.digits m ≠ []
q : b.digits (m / b) ≠ []
hm : ¬m = 0
⊢ (m % b :: b.digits (m / b)).getLast ⋯ = (b.digits (m / b)).getLast q

Tactic:
rw [List.getLast_cons]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma negDblY_of_Y_eq [NoZeroDivisors R] {P Q : Fin 3 → R} (hQz : Q z ≠ 0)
    (hx : P x * Q z ^ 2 = Q x * P z ^ 2) (hy : P y * Q z ^ 3 = Q y * P z ^ 3)
    (hy' : P y * Q z ^ 3 = W'.negY Q * P z ^ 3) : W'.negDblY P = (-W'.dblU P) ^ 3

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy : P y * Q z ^ 3 = Q y * P z ^ 3
hy' : P y * Q z ^ 3 = W'.negY Q * P z ^ 3
⊢ W'.negDblY P = (-W'.dblU P) ^ 3

Tactic:
rw [negDblY, dblX_of_Y_eq hQz hx hy hy', Y_eq_negY_of_Y_eq hQz hx hy hy']

Result:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy : P y * Q z ^ 3 = Q y * P z ^ 3
hy' : P y * Q z ^ 3 = W'.negY Q * P z ^ 3
⊢ -W'.dblU P * (W'.dblU P ^ 2 - P x * (W'.negY P - W'.negY P) ^ 2) + W'.negY P * (W'.negY P - W'.negY P) ^ 3 =
    (-W'.dblU P) ^ 3

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy : P y * Q z ^ 3 = Q y * P z ^ 3
hy' : P y * Q z ^ 3 = W'.negY Q * P z ^ 3
⊢ -W'.dblU P * (W'.dblU P ^ 2 - P x * (W'.negY P - W'.negY P) ^ 2) + W'.negY P * (W'.negY P - W'.negY P) ^ 3 =
    (-W'.dblU P) ^ 3

Tactic:
ring1

Result:
no goals
-- Mathlib/Analysis/Normed/Group/AddTorsor.lean
theorem dist_vadd_cancel_right (v₁ v₂ : V) (x : P) : dist (v₁ +ᵥ x) (v₂ +ᵥ x) = dist v₁ v₂

Proof state:
V : Type u_2
P : Type u_3
inst✝² : SeminormedAddCommGroup V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
v₁ v₂ : V
x : P
⊢ dist (v₁ +ᵥ x) (v₂ +ᵥ x) = dist v₁ v₂

Tactic:
rw [dist_eq_norm_vsub V, dist_eq_norm, vadd_vsub_vadd_cancel_right]

Result:
no goals
-- Mathlib/CategoryTheory/Adhesive.lean
theorem IsPushout.IsVanKampen.isPullback_of_mono_right [Mono g] {H : IsPushout f g h i}
    (H' : H.IsVanKampen) : IsPullback f g h i :=
  ((H' f (𝟙 _) (𝟙 _) f (𝟙 _) (𝟙 _) g h (IsPullback.of_vert_isIso ⟨by simp⟩)
      (IsKernelPair.id_of_mono g) ⟨rfl⟩ H.1 ⟨by simp⟩).mp
    (IsPushout.of_vert_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 g
H : IsPushout f g h i
H' : H.IsVanKampen
⊢ f ≫ 𝟙 X = 𝟙 W ≫ f

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Lattice.lean
theorem disjoint_iff_mul_eq_one {H₁ H₂ : Subgroup G} :
    Disjoint H₁ H₂ ↔ ∀ {x y : G}, x ∈ H₁ → y ∈ H₂ → x * y = 1 → x = 1 ∧ y = 1 :=
  disjoint_def'.trans
    ⟨fun h x y hx hy hxy =>
      let hx1 : x = 1 := h hx (H₂.inv_mem hy) (eq_inv_iff_mul_eq_one.mpr hxy)
      ⟨hx1, by simpa [hx1] using hxy⟩,
      fun h _ _ hx hy hxy => (h hx (H₂.inv_mem hy) (mul_inv_eq_one.mpr hxy)).1⟩

Proof state:
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
h : ∀ {x y : G}, x ∈ H₁ → y ∈ H₂ → x = y → x = 1
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
hxy : x * y = 1
hx1 : x = 1 := h hx (Subgroup.inv_mem H₂ hy) (eq_inv_iff_mul_eq_one.mpr hxy)
⊢ y = 1

Tactic:
simpa [hx1] using hxy

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean
theorem weightedHomogeneousComponent_apply [DecidableEq M] :
    weightedHomogeneousComponent w n φ =
      ∑ d ∈ φ.support with weight w d = n, monomial d (coeff d φ) :=
  letI := Classical.decEq M
  Finsupp.filter_eq_sum (fun d : σ →₀ ℕ => weight w d = n) φ |>.trans <| by convert rfl

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
inst✝ : DecidableEq M
this : DecidableEq M := Classical.decEq M
⊢ ∑ i ∈ Finset.filter (fun d => (weight w) d = n) φ.support, Finsupp.single i (φ i) =
    ∑ d ∈ Finset.filter (fun d => (weight w) d = n) φ.support, (monomial d) (coeff d φ)

Tactic:
convert rfl

Result:
no goals