harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/OreLocalization/Basic.lean
theorem smul_add (z : R[S⁻¹]) (x y : X[S⁻¹]) :
    z • (x + y) = z • x + z • y

Proof state:
case c.c.c.mk.mk.intro
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑(sa * s₁) = ra * ↑s₂
⊢ (r₃ /ₒ s₃) • ((sa • r₁ + ra • r₂) /ₒ (sa * s₁)) = (r₃ /ₒ s₃) • (sa • r₁ /ₒ (sa * s₁)) + (r₃ /ₒ s₃) • (r₂ /ₒ s₂)

Tactic:
rw [OreLocalization.expand r₂ s₂ ra (by rw [← ha]; apply SetLike.coe_mem)]

Result:
case c.c.c.mk.mk.intro
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑(sa * s₁) = ra * ↑s₂
⊢ (r₃ /ₒ s₃) • ((sa • r₁ + ra • r₂) /ₒ (sa * s₁)) =
    (r₃ /ₒ s₃) • (sa • r₁ /ₒ (sa * s₁)) + (r₃ /ₒ s₃) • (ra • r₂ /ₒ ⟨ra * ↑s₂, ⋯⟩)

Proof state:
case c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
z : OreLocalization S R
y : OreLocalization S X
r₁ : X
s₁ : ↥S
⊢ z • (r₁ /ₒ s₁ + y) = z • (r₁ /ₒ s₁) + z • y

Tactic:
induction' y with r₂ s₂

Result:
case c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
z : OreLocalization S R
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
⊢ z • (r₁ /ₒ s₁ + r₂ /ₒ s₂) = z • (r₁ /ₒ s₁) + z • (r₂ /ₒ s₂)

Proof state:
case c.c.c.mk.mk.intro
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑(sa * s₁) = ra * ↑s₂
⊢ oreNum r₃ (sa * s₁) • (sa • r₁ + ra • r₂) /ₒ (oreDenom r₃ (sa * s₁) * s₃) =
    oreNum r₃ (sa * s₁) • sa • r₁ /ₒ (oreDenom r₃ (sa * s₁) * s₃) +
      oreNum r₃ (sa * s₁) • ra • r₂ /ₒ (oreDenom r₃ (sa * s₁) * s₃)

Tactic:
simp only [smul_add, add_oreDiv]

Result:
no goals

Proof state:
case c.c.c.mk.mk.intro
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑(sa * s₁) = ra * ↑s₂
⊢ (r₃ /ₒ s₃) • ((sa • r₁ + ra • r₂) /ₒ (sa * s₁)) = (r₃ /ₒ s₃) • (r₁ /ₒ s₁) + (r₃ /ₒ s₃) • (r₂ /ₒ s₂)

Tactic:
rw [OreLocalization.expand' r₁ s₁ sa]

Result:
case c.c.c.mk.mk.intro
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑(sa * s₁) = ra * ↑s₂
⊢ (r₃ /ₒ s₃) • ((sa • r₁ + ra • r₂) /ₒ (sa * s₁)) = (r₃ /ₒ s₃) • (sa • r₁ /ₒ (sa * s₁)) + (r₃ /ₒ s₃) • (r₂ /ₒ s₂)
-- Mathlib/RingTheory/PrincipalIdealDomain.lean
theorem dvd_gcd (hx : z ∣ x) (hy : z ∣ y) : z ∣ gcd x y

Proof state:
R : Type u
inst✝¹ : CommRing R
x y z : R
inst✝ : IsPrincipal (Ideal.span {x, y})
hx : z ∣ x
hy : z ∣ y
⊢ z ∣ gcd x y

Tactic:
rw [← Ideal.span_singleton_le_span_singleton] at hx hy ⊢

Result:
R : Type u
inst✝¹ : CommRing R
x y z : R
inst✝ : IsPrincipal (Ideal.span {x, y})
hx : Ideal.span {x} ≤ Ideal.span {z}
hy : Ideal.span {y} ≤ Ideal.span {z}
⊢ Ideal.span {gcd x y} ≤ Ideal.span {z}

Proof state:
R : Type u
inst✝¹ : CommRing R
x y z : R
inst✝ : IsPrincipal (Ideal.span {x, y})
hx : Ideal.span {x} ≤ Ideal.span {z}
hy : Ideal.span {y} ≤ Ideal.span {z}
⊢ Ideal.span {gcd x y} ≤ Ideal.span {z}

Tactic:
rw [span_gcd, Ideal.span_insert, sup_le_iff]

Result:
R : Type u
inst✝¹ : CommRing R
x y z : R
inst✝ : IsPrincipal (Ideal.span {x, y})
hx : Ideal.span {x} ≤ Ideal.span {z}
hy : Ideal.span {y} ≤ Ideal.span {z}
⊢ Ideal.span {x} ≤ Ideal.span {z} ∧ Ideal.span {y} ≤ Ideal.span {z}

Proof state:
R : Type u
inst✝¹ : CommRing R
x y z : R
inst✝ : IsPrincipal (Ideal.span {x, y})
hx : Ideal.span {x} ≤ Ideal.span {z}
hy : Ideal.span {y} ≤ Ideal.span {z}
⊢ Ideal.span {x} ≤ Ideal.span {z} ∧ Ideal.span {y} ≤ Ideal.span {z}

Tactic:
exact ⟨hx, hy⟩

Result:
no goals
-- Mathlib/Analysis/Normed/Ring/Units.lean
theorem inverse_continuousAt (x : Rˣ) : ContinuousAt inverse (x : R)

Proof state:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
⊢ ContinuousAt inverse ↑x

Tactic:
have h_is_o : (fun t : R => inverse (↑x + t) - ↑x⁻¹) =o[𝓝 0] (fun _ => 1 : R → ℝ) :=
  (inverse_add_norm_diff_first_order x).trans_isLittleO (isLittleO_id_const one_ne_zero).norm_left

Result:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
h_is_o : (fun t => inverse (↑x + t) - ↑x⁻¹) =o[𝓝 0] fun x => 1
⊢ ContinuousAt inverse ↑x

Proof state:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
h_is_o : (fun t => inverse (↑x + t) - ↑x⁻¹) =o[𝓝 0] fun x => 1
h_lim : Tendsto (fun y => y - ↑x) (𝓝 ↑x) (𝓝 0)
⊢ Tendsto (fun e => ‖inverse e - ↑x⁻¹‖) (𝓝 ↑x) (𝓝 0)

Tactic:
simpa [Function.comp_def] using h_is_o.norm_left.tendsto_div_nhds_zero.comp h_lim

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
h_is_o : (fun t => inverse (↑x + t) - ↑x⁻¹) =o[𝓝 0] fun x => 1
⊢ Tendsto (fun y => y - ↑x) (𝓝 ↑x) (𝓝 0)

Tactic:
refine tendsto_zero_iff_norm_tendsto_zero.mpr ?_

Result:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
h_is_o : (fun t => inverse (↑x + t) - ↑x⁻¹) =o[𝓝 0] fun x => 1
⊢ Tendsto (fun x_1 => ‖x_1 - ↑x‖) (𝓝 ↑x) (𝓝 0)

Proof state:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
h_is_o : (fun t => inverse (↑x + t) - ↑x⁻¹) =o[𝓝 0] fun x => 1
⊢ ContinuousAt inverse ↑x

Tactic:
have h_lim : Tendsto (fun y : R => y - x) (𝓝 x) (𝓝 0) := by
  refine tendsto_zero_iff_norm_tendsto_zero.mpr ?_
  exact tendsto_iff_norm_sub_tendsto_zero.mp tendsto_id

Result:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
h_is_o : (fun t => inverse (↑x + t) - ↑x⁻¹) =o[𝓝 0] fun x => 1
h_lim : Tendsto (fun y => y - ↑x) (𝓝 ↑x) (𝓝 0)
⊢ ContinuousAt inverse ↑x

Proof state:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
h_is_o : (fun t => inverse (↑x + t) - ↑x⁻¹) =o[𝓝 0] fun x => 1
h_lim : Tendsto (fun y => y - ↑x) (𝓝 ↑x) (𝓝 0)
⊢ ContinuousAt inverse ↑x

Tactic:
rw [ContinuousAt, tendsto_iff_norm_sub_tendsto_zero, inverse_unit]

Result:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
h_is_o : (fun t => inverse (↑x + t) - ↑x⁻¹) =o[𝓝 0] fun x => 1
h_lim : Tendsto (fun y => y - ↑x) (𝓝 ↑x) (𝓝 0)
⊢ Tendsto (fun e => ‖inverse e - ↑x⁻¹‖) (𝓝 ↑x) (𝓝 0)

Proof state:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
h_is_o : (fun t => inverse (↑x + t) - ↑x⁻¹) =o[𝓝 0] fun x => 1
⊢ Tendsto (fun x_1 => ‖x_1 - ↑x‖) (𝓝 ↑x) (𝓝 0)

Tactic:
exact tendsto_iff_norm_sub_tendsto_zero.mp tendsto_id

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem iSup_ne_bot_subtype (f : ι → α) : ⨆ i : { i // f i ≠ ⊥ }, f i = ⨆ i, f i

Proof state:
case neg
α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
f : ι → α
htriv : ¬∀ (i : ι), f i = ⊥
i : ι
hi : ¬f i = ⊥
⊢ ∃ i', f i ≤ f ↑i'

Tactic:
exact ⟨⟨i, hi⟩, rfl.le⟩

Result:
no goals

Proof state:
case pos
α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
f : ι → α
htriv : ∀ (i : ι), f i = ⊥
⊢ ⨆ i, f ↑i = ⨆ i, f i

Tactic:
simp only [iSup_bot, (funext htriv : f = _)]

Result:
no goals

Proof state:
case pos.intro
α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
f : ι → α
htriv : ¬∀ (i : ι), f i = ⊥
i : ι
hi : f i = ⊥
i₀ : ι
hi₀ : ¬f i₀ = ⊥
⊢ ∃ i', ⊥ ≤ f ↑i'

Tactic:
exact ⟨⟨i₀, hi₀⟩, bot_le⟩

Result:
no goals

Proof state:
case pos
α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
f : ι → α
htriv : ¬∀ (i : ι), f i = ⊥
i : ι
hi : f i = ⊥
⊢ ∃ i', f i ≤ f ↑i'

Tactic:
rw [hi]

Result:
case pos
α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
f : ι → α
htriv : ¬∀ (i : ι), f i = ⊥
i : ι
hi : f i = ⊥
⊢ ∃ i', ⊥ ≤ f ↑i'

Proof state:
case pos
α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
f : ι → α
htriv : ¬∀ (i : ι), f i = ⊥
i : ι
hi : f i = ⊥
⊢ ∃ i', ⊥ ≤ f ↑i'

Tactic:
obtain ⟨i₀, hi₀⟩ := not_forall.mp htriv

Result:
case pos.intro
α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
f : ι → α
htriv : ¬∀ (i : ι), f i = ⊥
i : ι
hi : f i = ⊥
i₀ : ι
hi₀ : ¬f i₀ = ⊥
⊢ ∃ i', ⊥ ≤ f ↑i'

Proof state:
case neg
α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
f : ι → α
htriv : ¬∀ (i : ι), f i = ⊥
⊢ ⨆ i, f ↑i = ⨆ i, f i

Tactic:
refine (iSup_comp_le f _).antisymm (iSup_mono' fun i => ?_)

Result:
case neg
α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
f : ι → α
htriv : ¬∀ (i : ι), f i = ⊥
i : ι
⊢ ∃ i', f i ≤ f ↑i'

Proof state:
α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
f : ι → α
⊢ ⨆ i, f ↑i = ⨆ i, f i

Tactic:
by_cases htriv : ∀ i, f i = ⊥

Result:
case pos
α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
f : ι → α
htriv : ∀ (i : ι), f i = ⊥
⊢ ⨆ i, f ↑i = ⨆ i, f i

case neg
α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
f : ι → α
htriv : ¬∀ (i : ι), f i = ⊥
⊢ ⨆ i, f ↑i = ⨆ i, f i

Proof state:
case neg
α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
f : ι → α
htriv : ¬∀ (i : ι), f i = ⊥
i : ι
⊢ ∃ i', f i ≤ f ↑i'

Tactic:
by_cases hi : f i = ⊥

Result:
case pos
α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
f : ι → α
htriv : ¬∀ (i : ι), f i = ⊥
i : ι
hi : f i = ⊥
⊢ ∃ i', f i ≤ f ↑i'

case neg
α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
f : ι → α
htriv : ¬∀ (i : ι), f i = ⊥
i : ι
hi : ¬f i = ⊥
⊢ ∃ i', f i ≤ f ↑i'
-- Mathlib/Data/Nat/GCD/Basic.lean
theorem gcd_self_sub_right {m n : ℕ} (h : m ≤ n) : gcd n (n - m) = gcd n m

Proof state:
m n : ℕ
h : m ≤ n
⊢ n.gcd (n - m) = n.gcd m

Tactic:
rw [gcd_comm, gcd_self_sub_left h, gcd_comm]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Infsep.lean
theorem Nontrivial.einfsep_exists_of_finite [Finite s] (hs : s.Nontrivial) :
    ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.einfsep = edist x y

Proof state:
α : Type u_1
inst✝¹ : EDist α
s : Set α
inst✝ : Finite ↑s
hs : s.Nontrivial
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.einfsep = edist x y

Tactic:
classical
  cases nonempty_fintype s
  simp_rw [einfsep_of_fintype]
  rcases Finset.exists_mem_eq_inf s.offDiag.toFinset (by simpa) (uncurry edist) with ⟨w, hxy, hed⟩
  simp_rw [mem_toFinset] at hxy
  exact ⟨w.fst, hxy.1, w.snd, hxy.2.1, hxy.2.2, hed⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : EDist α
s : Set α
inst✝ : Finite ↑s
hs : s.Nontrivial
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.einfsep = edist x y

Tactic:
cases nonempty_fintype s

Result:
case intro
α : Type u_1
inst✝¹ : EDist α
s : Set α
inst✝ : Finite ↑s
hs : s.Nontrivial
val✝ : Fintype ↑s
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.einfsep = edist x y

Proof state:
case intro
α : Type u_1
inst✝¹ : EDist α
s : Set α
inst✝ : Finite ↑s
hs : s.Nontrivial
val✝ : Fintype ↑s
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.einfsep = edist x y

Tactic:
simp_rw [einfsep_of_fintype]

Result:
case intro
α : Type u_1
inst✝¹ : EDist α
s : Set α
inst✝ : Finite ↑s
hs : s.Nontrivial
val✝ : Fintype ↑s
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.offDiag.toFinset.inf (uncurry edist) = edist x y

Proof state:
case intro.intro.intro
α : Type u_1
inst✝¹ : EDist α
s : Set α
inst✝ : Finite ↑s
hs : s.Nontrivial
val✝ : Fintype ↑s
w : α × α
hxy : w ∈ s.offDiag.toFinset
hed : s.offDiag.toFinset.inf (uncurry edist) = uncurry edist w
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.offDiag.toFinset.inf (uncurry edist) = edist x y

Tactic:
simp_rw [mem_toFinset] at hxy

Result:
case intro.intro.intro
α : Type u_1
inst✝¹ : EDist α
s : Set α
inst✝ : Finite ↑s
hs : s.Nontrivial
val✝ : Fintype ↑s
w : α × α
hed : s.offDiag.toFinset.inf (uncurry edist) = uncurry edist w
hxy : w ∈ s.offDiag
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.offDiag.toFinset.inf (uncurry edist) = edist x y

Proof state:
case intro.intro.intro
α : Type u_1
inst✝¹ : EDist α
s : Set α
inst✝ : Finite ↑s
hs : s.Nontrivial
val✝ : Fintype ↑s
w : α × α
hed : s.offDiag.toFinset.inf (uncurry edist) = uncurry edist w
hxy : w ∈ s.offDiag
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.offDiag.toFinset.inf (uncurry edist) = edist x y

Tactic:
exact ⟨w.fst, hxy.1, w.snd, hxy.2.1, hxy.2.2, hed⟩

Result:
no goals

Proof state:
case intro
α : Type u_1
inst✝¹ : EDist α
s : Set α
inst✝ : Finite ↑s
hs : s.Nontrivial
val✝ : Fintype ↑s
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.offDiag.toFinset.inf (uncurry edist) = edist x y

Tactic:
rcases Finset.exists_mem_eq_inf s.offDiag.toFinset (by simpa) (uncurry edist) with ⟨w, hxy, hed⟩

Result:
case intro.intro.intro
α : Type u_1
inst✝¹ : EDist α
s : Set α
inst✝ : Finite ↑s
hs : s.Nontrivial
val✝ : Fintype ↑s
w : α × α
hxy : w ∈ s.offDiag.toFinset
hed : s.offDiag.toFinset.inf (uncurry edist) = uncurry edist w
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.offDiag.toFinset.inf (uncurry edist) = edist x y

Proof state:
α : Type u_1
inst✝¹ : EDist α
s : Set α
inst✝ : Finite ↑s
hs : s.Nontrivial
val✝ : Fintype ↑s
⊢ s.offDiag.toFinset.Nonempty

Tactic:
simpa

Result:
no goals
-- Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean
theorem coeff_smul {S} [SMulZeroClass S k] (r : S) (p : SkewMonoidAlgebra k G) (a : G) :
    coeff (r • p) a = r • coeff p a

Proof state:
k : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid k
S : Type u_3
inst✝ : SMulZeroClass S k
r : S
p : SkewMonoidAlgebra k G
a : G
⊢ (r • p).coeff a = r • p.coeff a

Tactic:
rcases p

Result:
case ofFinsupp
k : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid k
S : Type u_3
inst✝ : SMulZeroClass S k
r : S
a : G
toFinsupp✝ : G →₀ k
⊢ (r • { toFinsupp := toFinsupp✝ }).coeff a = r • { toFinsupp := toFinsupp✝ }.coeff a

Proof state:
case ofFinsupp
k : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid k
S : Type u_3
inst✝ : SMulZeroClass S k
r : S
a : G
toFinsupp✝ : G →₀ k
⊢ (r • toFinsupp✝) a = r • toFinsupp✝ a

Tactic:
exact Finsupp.smul_apply _ _ _

Result:
no goals

Proof state:
case ofFinsupp
k : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid k
S : Type u_3
inst✝ : SMulZeroClass S k
r : S
a : G
toFinsupp✝ : G →₀ k
⊢ (r • { toFinsupp := toFinsupp✝ }).coeff a = r • { toFinsupp := toFinsupp✝ }.coeff a

Tactic:
simp_rw [← ofFinsupp_smul, coeff]

Result:
case ofFinsupp
k : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid k
S : Type u_3
inst✝ : SMulZeroClass S k
r : S
a : G
toFinsupp✝ : G →₀ k
⊢ (r • toFinsupp✝) a = r • toFinsupp✝ a
-- Mathlib/FieldTheory/PurelyInseparable/Basic.lean
theorem AlgEquiv.isPurelyInseparable (e : K ≃ₐ[F] E) [IsPurelyInseparable F K] :
    IsPurelyInseparable F E

Proof state:
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : Ring E
inst✝³ : Algebra F E
K : Type u_3
inst✝² : Ring K
inst✝¹ : Algebra F K
e : K ≃ₐ[F] E
inst✝ : IsPurelyInseparable F K
⊢ IsPurelyInseparable F E

Tactic:
refine ⟨⟨fun _ ↦ by rw [← isIntegral_algEquiv e.symm]; exact IsPurelyInseparable.isIntegral' F _⟩,
  fun x h ↦ ?_⟩

Result:
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : Ring E
inst✝³ : Algebra F E
K : Type u_3
inst✝² : Ring K
inst✝¹ : Algebra F K
e : K ≃ₐ[F] E
inst✝ : IsPurelyInseparable F K
x : E
h : IsSeparable F x
⊢ x ∈ (algebraMap F E).range

Proof state:
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : Ring E
inst✝³ : Algebra F E
K : Type u_3
inst✝² : Ring K
inst✝¹ : Algebra F K
e : K ≃ₐ[F] E
inst✝ : IsPurelyInseparable F K
x✝ : E
⊢ IsIntegral F (e.symm x✝)

Tactic:
exact IsPurelyInseparable.isIntegral' F _

Result:
no goals

Proof state:
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : Ring E
inst✝³ : Algebra F E
K : Type u_3
inst✝² : Ring K
inst✝¹ : Algebra F K
e : K ≃ₐ[F] E
inst✝ : IsPurelyInseparable F K
x : E
h : (minpoly F (e.symm x)).Separable
⊢ x ∈ (algebraMap F E).range

Tactic:
simpa only [RingHom.mem_range, algebraMap_eq_apply] using IsPurelyInseparable.inseparable F _ h

Result:
no goals

Proof state:
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : Ring E
inst✝³ : Algebra F E
K : Type u_3
inst✝² : Ring K
inst✝¹ : Algebra F K
e : K ≃ₐ[F] E
inst✝ : IsPurelyInseparable F K
x : E
h : IsSeparable F x
⊢ x ∈ (algebraMap F E).range

Tactic:
rw [IsSeparable, ← minpoly.algEquiv_eq e.symm] at h

Result:
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : Ring E
inst✝³ : Algebra F E
K : Type u_3
inst✝² : Ring K
inst✝¹ : Algebra F K
e : K ≃ₐ[F] E
inst✝ : IsPurelyInseparable F K
x : E
h : (minpoly F (e.symm x)).Separable
⊢ x ∈ (algebraMap F E).range

Proof state:
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : Ring E
inst✝³ : Algebra F E
K : Type u_3
inst✝² : Ring K
inst✝¹ : Algebra F K
e : K ≃ₐ[F] E
inst✝ : IsPurelyInseparable F K
x✝ : E
⊢ IsIntegral F x✝

Tactic:
rw [← isIntegral_algEquiv e.symm]

Result:
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : Ring E
inst✝³ : Algebra F E
K : Type u_3
inst✝² : Ring K
inst✝¹ : Algebra F K
e : K ≃ₐ[F] E
inst✝ : IsPurelyInseparable F K
x✝ : E
⊢ IsIntegral F (e.symm x✝)
-- Mathlib/Algebra/Group/Fin/Tuple.lean
@[simp] lemma cons_add (x : α) (v : Fin n → α) (w : Fin n.succ → α) :
    vecCons x v + w = vecCons (x + vecHead w) (v + vecTail w)

Proof state:
case h
α : Type u_1
n : ℕ
inst✝ : Add α
x : α
v : Fin n → α
w : Fin n.succ → α
i : Fin n.succ
⊢ (vecCons x v + w) i = vecCons (x + vecHead w) (v + vecTail w) i

Tactic:
refine i.cases ?_ ?_ <;> simp [vecHead, vecTail]

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
inst✝ : Add α
x : α
v : Fin n → α
w : Fin n.succ → α
⊢ vecCons x v + w = vecCons (x + vecHead w) (v + vecTail w)

Tactic:
ext i

Result:
case h
α : Type u_1
n : ℕ
inst✝ : Add α
x : α
v : Fin n → α
w : Fin n.succ → α
i : Fin n.succ
⊢ (vecCons x v + w) i = vecCons (x + vecHead w) (v + vecTail w) i
-- Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean
theorem mul_eq_mul_iff_eq_and_eq [MulLeftStrictMono α]
    [MulRightStrictMono α] {a b c d : α} (hac : a ≤ c) (hbd : b ≤ d) :
    a * b = c * d ↔ a = c ∧ b = d

Proof state:
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
hac : a ≤ c
hbd : b ≤ d
this✝ : MulLeftMono α
this : MulRightMono α
⊢ a * b = c * d ↔ a = c ∧ b = d

Tactic:
rw [le_antisymm_iff, eq_true (mul_le_mul' hac hbd), true_and, mul_le_mul_iff_of_ge hac hbd]

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
hac : a ≤ c
hbd : b ≤ d
this : MulLeftMono α
⊢ a * b = c * d ↔ a = c ∧ b = d

Tactic:
haveI := mulRightMono_of_mulRightStrictMono α

Result:
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
hac : a ≤ c
hbd : b ≤ d
this✝ : MulLeftMono α
this : MulRightMono α
⊢ a * b = c * d ↔ a = c ∧ b = d

Proof state:
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
hac : a ≤ c
hbd : b ≤ d
⊢ a * b = c * d ↔ a = c ∧ b = d

Tactic:
haveI := mulLeftMono_of_mulLeftStrictMono α

Result:
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
hac : a ≤ c
hbd : b ≤ d
this : MulLeftMono α
⊢ a * b = c * d ↔ a = c ∧ b = d
-- Mathlib/Data/Set/Finite/Basic.lean
lemma Finite.exists_not_mem (hs : s.Finite) : ∃ a, a ∉ s

Proof state:
α : Type u
s : Set α
inst✝ : Infinite α
hs : s.Finite
⊢ ∃ a, a ∉ s

Tactic:
by_contra! h

Result:
α : Type u
s : Set α
inst✝ : Infinite α
hs : s.Finite
h : ∀ (a : α), a ∈ s
⊢ False

Proof state:
α : Type u
s : Set α
inst✝ : Infinite α
hs : s.Finite
h : ∀ (a : α), a ∈ s
⊢ False

Tactic:
exact infinite_univ (hs.subset fun a _ ↦ h _)

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean
lemma addLECancellable_iff_ne_top [Nonempty α] [Preorder α]
    [ContravariantClass α α (· + ·) (· ≤ ·)] : AddLECancellable x ↔ x ≠ ⊤ where
  mp

Proof state:
α : Type u
inst✝³ : Add α
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : ContravariantClass α α (fun x1 x2 => x1 + x2) fun x1 x2 => x1 ≤ x2
h : AddLECancellable ⊤
⊢ False

Tactic:
exact (coe_lt_top <| Classical.arbitrary _).not_le <| h <| by simp

Result:
no goals

Proof state:
α : Type u
inst✝³ : Add α
x : WithTop α
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : ContravariantClass α α (fun x1 x2 => x1 + x2) fun x1 x2 => x1 ≤ x2
⊢ AddLECancellable x → x ≠ ⊤

Tactic:
rintro h rfl

Result:
α : Type u
inst✝³ : Add α
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : ContravariantClass α α (fun x1 x2 => x1 + x2) fun x1 x2 => x1 ≤ x2
h : AddLECancellable ⊤
⊢ False

Proof state:
α : Type u
inst✝³ : Add α
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : ContravariantClass α α (fun x1 x2 => x1 + x2) fun x1 x2 => x1 ≤ x2
h : AddLECancellable ⊤
⊢ ⊤ + ⊤ ≤ ⊤ + ↑(Classical.arbitrary α)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey?_alter (h : m.1.WF) {k k' : α} {f : Option β → Option β} :
    (Const.alter m k f).getKey? k' =
      if k == k' then
        if (f (Const.get? m k)).isSome then some k else none
      else
        m.getKey? k'

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
h : m.val.WF
k k' : α
f : Option β → Option β
⊢ (alter m k f).getKey? k' =
    if (k == k') = true then if (f (get? m k)).isSome = true then some k else none else m.getKey? k'

Tactic:
simp_to_model [Const.alter] using List.Const.getKey?_alterKey

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean
theorem two_mul_arctan {x : ℝ} (h₁ : -1 < x) (h₂ : x < 1) :
    2 * arctan x = arctan (2 * x / (1 - x ^ 2))

Proof state:
x : ℝ
h₁ : -1 < x
h₂ : x < 1
⊢ x * x < 1

Tactic:
nlinarith

Result:
no goals

Proof state:
x : ℝ
h₁ : -1 < x
h₂ : x < 1
⊢ 2 * arctan x = arctan (2 * x / (1 - x ^ 2))

Tactic:
rw [two_mul, arctan_add (by nlinarith)]

Result:
x : ℝ
h₁ : -1 < x
h₂ : x < 1
⊢ arctan ((x + x) / (1 - x * x)) = arctan (2 * x / (1 - x ^ 2))

Proof state:
case e_x
x : ℝ
h₁ : -1 < x
h₂ : x < 1
⊢ (x + x) / (1 - x * x) = 2 * x / (1 - x ^ 2)

Tactic:
ring

Result:
no goals

Proof state:
x : ℝ
h₁ : -1 < x
h₂ : x < 1
⊢ arctan ((x + x) / (1 - x * x)) = arctan (2 * x / (1 - x ^ 2))

Tactic:
congr 1

Result:
case e_x
x : ℝ
h₁ : -1 < x
h₂ : x < 1
⊢ (x + x) / (1 - x * x) = 2 * x / (1 - x ^ 2)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/RefVec.lean
theorem get_push_ref_lt (s : RefVec aig len) (ref : AIG.Ref aig) (idx : Nat)
    (hidx : idx < len) :
    (s.push ref).get idx (by omega) = s.get idx hidx

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefVec len
ref : aig.Ref
idx : Nat
hidx : idx < len
⊢ idx < len + 1

Tactic:
omega

Result:
no goals

Proof state:
case mk
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefVec len
idx : Nat
hidx : idx < len
gate✝ : Nat
hgate✝ : gate✝ < aig.decls.size
⊢ (s.refs.push gate✝)[idx] = s.refs[idx]

Tactic:
rw [Array.getElem_push_lt]

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefVec len
ref : aig.Ref
idx : Nat
hidx : idx < len
⊢ (s.push ref).get idx ⋯ = s.get idx hidx

Tactic:
simp only [get, push, Ref.mk.injEq]

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefVec len
ref : aig.Ref
idx : Nat
hidx : idx < len
⊢ (s.refs.push ref.gate)[idx] = s.refs[idx]

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefVec len
ref : aig.Ref
idx : Nat
hidx : idx < len
⊢ (s.refs.push ref.gate)[idx] = s.refs[idx]

Tactic:
cases ref

Result:
case mk
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefVec len
idx : Nat
hidx : idx < len
gate✝ : Nat
hgate✝ : gate✝ < aig.decls.size
⊢ (s.refs.push { gate := gate✝, hgate := hgate✝ }.gate)[idx] = s.refs[idx]

Proof state:
case mk
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefVec len
idx : Nat
hidx : idx < len
gate✝ : Nat
hgate✝ : gate✝ < aig.decls.size
⊢ (s.refs.push { gate := gate✝, hgate := hgate✝ }.gate)[idx] = s.refs[idx]

Tactic:
simp only [Ref.mk.injEq]

Result:
case mk
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefVec len
idx : Nat
hidx : idx < len
gate✝ : Nat
hgate✝ : gate✝ < aig.decls.size
⊢ (s.refs.push gate✝)[idx] = s.refs[idx]