harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIxxMod_trans {x₁ x₂ x₃ x₄ : α}
    (h₁₂₃ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ∧ ¬toIcoMod hp x₃ x₂ ≤ toIocMod hp x₃ x₁)
    (h₂₃₄ : toIcoMod hp x₂ x₄ ≤ toIocMod hp x₂ x₃ ∧ ¬toIcoMod hp x₃ x₄ ≤ toIocMod hp x₃ x₂) :
    toIcoMod hp x₁ x₄ ≤ toIocMod hp x₁ x₃ ∧ ¬toIcoMod hp x₃ x₄ ≤ toIocMod hp x₃ x₁

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
x₁ x₂ x₃ x₄ : α
h₁₂₃ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ∧ ¬toIcoMod hp x₃ x₂ ≤ toIocMod hp x₃ x₁
h₂₃₄ : toIcoMod hp x₂ x₄ ≤ toIocMod hp x₂ x₃ ∧ ¬toIcoMod hp x₃ x₄ ≤ toIocMod hp x₃ x₂
h : ¬x₃ ≡ x₂ [PMOD p]
h₁₂₃' : toIcoMod hp x₃ x₁ ≤ toIocMod hp x₃ x₂
⊢ toIcoMod hp x₁ x₄ ≤ toIocMod hp x₁ x₃

Tactic:
have h₂₃₄' := toIxxMod_cyclic_left _ (toIxxMod_cyclic_left _ h₂₃₄.1)

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
x₁ x₂ x₃ x₄ : α
h₁₂₃ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ∧ ¬toIcoMod hp x₃ x₂ ≤ toIocMod hp x₃ x₁
h₂₃₄ : toIcoMod hp x₂ x₄ ≤ toIocMod hp x₂ x₃ ∧ ¬toIcoMod hp x₃ x₄ ≤ toIocMod hp x₃ x₂
h : ¬x₃ ≡ x₂ [PMOD p]
h₁₂₃' : toIcoMod hp x₃ x₁ ≤ toIocMod hp x₃ x₂
h₂₃₄' : toIcoMod hp x₃ x₂ ≤ toIocMod hp x₃ x₄
⊢ toIcoMod hp x₁ x₄ ≤ toIocMod hp x₁ x₃
-- Mathlib/Order/Birkhoff.lean
@[simp] lemma infIrred_Ici (a : α) : InfIrred (Ici a)

Proof state:
α : Type u_1
inst✝ : PartialOrder α
a : α
⊢ InfIrred (Ici a)

Tactic:
refine ⟨fun h ↦ Ici_ne_top h.eq_top, fun s t hst ↦ ?_⟩

Result:
α : Type u_1
inst✝ : PartialOrder α
a : α
s t : UpperSet α
hst : s ⊓ t = Ici a
⊢ s = Ici a ∨ t = Ici a

Proof state:
α : Type u_1
inst✝ : PartialOrder α
a : α
s t : UpperSet α
hst : s ⊓ t = Ici a
⊢ s = Ici a ∨ t = Ici a

Tactic:
have := mem_Ici_iff.2 (le_refl a)

Result:
α : Type u_1
inst✝ : PartialOrder α
a : α
s t : UpperSet α
hst : s ⊓ t = Ici a
this : a ∈ Ici a
⊢ s = Ici a ∨ t = Ici a

Proof state:
α : Type u_1
inst✝ : PartialOrder α
a : α
s t : UpperSet α
hst : s ⊓ t = Ici a
this : a ∈ s ⊓ t
⊢ s = Ici a ∨ t = Ici a

Tactic:
exact this.imp (fun ha ↦ le_antisymm (le_Ici.2 ha) <| hst.ge.trans inf_le_left) fun ha ↦
    le_antisymm (le_Ici.2 ha) <| hst.ge.trans inf_le_right

Result:
no goals

Proof state:
α : Type u_1
inst✝ : PartialOrder α
a : α
s t : UpperSet α
hst : s ⊓ t = Ici a
this : a ∈ Ici a
⊢ s = Ici a ∨ t = Ici a

Tactic:
rw [← hst] at this

Result:
α : Type u_1
inst✝ : PartialOrder α
a : α
s t : UpperSet α
hst : s ⊓ t = Ici a
this : a ∈ s ⊓ t
⊢ s = Ici a ∨ t = Ici a
-- Mathlib/Data/Multiset/UnionInter.lean
lemma cons_union_distrib (a : α) (s t : Multiset α) : a ::ₘ (s ∪ t) = a ::ₘ s ∪ a ::ₘ t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
⊢ a ::ₘ (s ∪ t) = a ::ₘ s ∪ a ::ₘ t

Tactic:
simpa using add_union_distrib (a ::ₘ 0) s t

Result:
no goals
-- Mathlib/Data/Int/Init.lean
lemma dvd_div_of_mul_dvd (h : a * b ∣ c) : b ∣ c / a

Proof state:
case inr.intro
a b : ℤ
ha : ¬a = 0
d : ℤ
⊢ b ∣ a * b * d / a

Tactic:
simp [Int.mul_assoc, ha]

Result:
no goals

Proof state:
case inl
b c : ℤ
h : 0 * b ∣ c
⊢ b ∣ c / 0

Tactic:
simp

Result:
no goals

Proof state:
a b c : ℤ
h : a * b ∣ c
⊢ b ∣ c / a

Tactic:
obtain rfl | ha := Decidable.em (a = 0)

Result:
case inl
b c : ℤ
h : 0 * b ∣ c
⊢ b ∣ c / 0

case inr
a b c : ℤ
h : a * b ∣ c
ha : ¬a = 0
⊢ b ∣ c / a

Proof state:
case inr
a b c : ℤ
h : a * b ∣ c
ha : ¬a = 0
⊢ b ∣ c / a

Tactic:
obtain ⟨d, rfl⟩ := h

Result:
case inr.intro
a b : ℤ
ha : ¬a = 0
d : ℤ
⊢ b ∣ a * b * d / a
-- Mathlib/Geometry/Manifold/PartitionOfUnity.lean
theorem contDiffAt_finsum {s : Set E} (f : SmoothPartitionOfUnity ι 𝓘(ℝ, E) E s) {x₀ : E}
    {g : ι → E → F} (hφ : ∀ i, x₀ ∈ tsupport (f i) → ContDiffAt ℝ n (g i) x₀) :
    ContDiffAt ℝ n (fun x ↦ ∑ᶠ i, f i x • g i x) x₀

Proof state:
ι : Type uι
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ∞
s : Set E
f : SmoothPartitionOfUnity ι 𝓘(ℝ, E) E s
x₀ : E
g : ι → E → F
hφ : ∀ (i : ι), x₀ ∈ tsupport ⇑(f i) → ContMDiffAt 𝓘(ℝ, E) 𝓘(ℝ, F) (↑n) (g i) x₀
⊢ ContMDiffAt 𝓘(ℝ, E) 𝓘(ℝ, F) (↑n) (fun x => ∑ᶠ (i : ι), (f i) x • g i x) x₀

Tactic:
exact f.contMDiffAt_finsum hφ

Result:
no goals

Proof state:
ι : Type uι
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ∞
s : Set E
f : SmoothPartitionOfUnity ι 𝓘(ℝ, E) E s
x₀ : E
g : ι → E → F
hφ : ∀ (i : ι), x₀ ∈ tsupport ⇑(f i) → ContDiffAt ℝ (↑n) (g i) x₀
⊢ ContDiffAt ℝ (↑n) (fun x => ∑ᶠ (i : ι), (f i) x • g i x) x₀

Tactic:
simp only [← contMDiffAt_iff_contDiffAt] at *

Result:
ι : Type uι
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ∞
s : Set E
f : SmoothPartitionOfUnity ι 𝓘(ℝ, E) E s
x₀ : E
g : ι → E → F
hφ : ∀ (i : ι), x₀ ∈ tsupport ⇑(f i) → ContMDiffAt 𝓘(ℝ, E) 𝓘(ℝ, F) (↑n) (g i) x₀
⊢ ContMDiffAt 𝓘(ℝ, E) 𝓘(ℝ, F) (↑n) (fun x => ∑ᶠ (i : ι), (f i) x • g i x) x₀
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem aleph0_le_card {o} : ℵ₀ ≤ card o ↔ ω ≤ o

Proof state:
o : Ordinal.{u_1}
⊢ ℵ₀ ≤ o.card ↔ ω ≤ o

Tactic:
rw [← ord_le, ord_aleph0]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma add_sub_one_le_mul (ha : a ≠ 0) (hb : b ≠ 0) : a + b - 1 ≤ a * b

Proof state:
case zero
b : ℕ
hb : b ≠ 0
ha : 0 ≠ 0
⊢ 0 + b - 1 ≤ 0 * b

Tactic:
cases ha rfl

Result:
no goals

Proof state:
case succ
b : ℕ
hb : b ≠ 0
n✝ : ℕ
ha : n✝ + 1 ≠ 0
⊢ n✝ + 1 + b - 1 ≤ (n✝ + 1) * b

Tactic:
rw [succ_add, Nat.add_one_sub_one, succ_mul]

Result:
case succ
b : ℕ
hb : b ≠ 0
n✝ : ℕ
ha : n✝ + 1 ≠ 0
⊢ n✝ + b ≤ n✝ * b + b

Proof state:
case succ
b : ℕ
hb : b ≠ 0
n✝ : ℕ
ha : n✝ + 1 ≠ 0
⊢ n✝ + b ≤ n✝ * b + b

Tactic:
exact Nat.add_le_add_right (Nat.le_mul_of_pos_right _ <| Nat.pos_iff_ne_zero.2 hb) _

Result:
no goals

Proof state:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a + b - 1 ≤ a * b

Tactic:
cases a

Result:
case zero
b : ℕ
hb : b ≠ 0
ha : 0 ≠ 0
⊢ 0 + b - 1 ≤ 0 * b

case succ
b : ℕ
hb : b ≠ 0
n✝ : ℕ
ha : n✝ + 1 ≠ 0
⊢ n✝ + 1 + b - 1 ≤ (n✝ + 1) * b
-- Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean
theorem toComplex_div_re (x y : ℤ[i]) : ((x / y : ℤ[i]) : ℂ).re = round (x / y : ℂ).re

Proof state:
x y : ℤ[i]
⊢ (toComplex (x / y)).re = ↑(round (toComplex x / toComplex y).re)

Tactic:
rw [div_def, ← @Rat.round_cast ℝ _ _]

Result:
x y : ℤ[i]
⊢ (toComplex { re := round ↑(↑(x * star y).re / ↑(norm y)), im := round (↑(x * star y).im / ↑(norm y)) }).re =
    ↑(round (toComplex x / toComplex y).re)

Proof state:
x y : ℤ[i]
⊢ (toComplex { re := round ↑(↑(x * star y).re / ↑(norm y)), im := round (↑(x * star y).im / ↑(norm y)) }).re =
    ↑(round (toComplex x / toComplex y).re)

Tactic:
simp [-Rat.round_cast, mul_assoc, div_eq_mul_inv, mul_add, add_mul]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem normAtPlace_nonneg (w : InfinitePlace K) (x : mixedSpace K) :
    0 ≤ normAtPlace w x

Proof state:
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x : mixedSpace K
⊢ 0 ≤ (normAtPlace w) x

Tactic:
rw [normAtPlace, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk]

Result:
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x : mixedSpace K
⊢ 0 ≤ if hw : w.IsReal then ‖x.1 ⟨w, hw⟩‖ else ‖x.2 ⟨w, ⋯⟩‖

Proof state:
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x : mixedSpace K
⊢ 0 ≤ if hw : w.IsReal then ‖x.1 ⟨w, hw⟩‖ else ‖x.2 ⟨w, ⋯⟩‖

Tactic:
split_ifs <;> exact norm_nonneg _

Result:
no goals
-- Mathlib/NumberTheory/Padics/MahlerBasis.lean
/-- Evaluation of a Mahler series is just the pointwise sum. -/
lemma mahlerSeries_apply (ha : Tendsto a atTop (𝓝 0)) (x : ℤ_[p]) :
    mahlerSeries a x = ∑' n, mahler n x • a n

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℚ_[p] E
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
x : ℤ_[p]
⊢ (mahlerSeries a) x = ∑' (n : ℕ), (mahler n) x • a n

Tactic:
simp only [mahlerSeries, ← ContinuousMap.tsum_apply (hasSum_mahlerSeries ha).summable,
  mahlerTerm_apply]

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/lpSpace.lean
theorem norm_sub_norm_compl_sub_single (hp : 0 < p.toReal) (f : lp E p) (s : Finset α) :
    ‖f‖ ^ p.toReal - ‖f - ∑ i ∈ s, lp.single p i (f i)‖ ^ p.toReal =
      ∑ i ∈ s, ‖f i‖ ^ p.toReal

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
hp : 0 < p.toReal
f : ↥(lp E p)
s : Finset α
F : α → ℝ := fun i => ‖↑f i‖ ^ p.toReal - ‖↑(f - ∑ i ∈ s, lp.single p i (↑f i)) i‖ ^ p.toReal
i : α
hi : i ∉ s
⊢ ‖↑f i‖ ^ p.toReal - ‖↑f i - if i ∈ s then ↑f i else 0‖ ^ p.toReal = 0

Tactic:
simp only [if_neg hi, sub_zero, sub_self]

Result:
no goals

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
hp : 0 < p.toReal
f : ↥(lp E p)
s : Finset α
⊢ ‖f‖ ^ p.toReal - ‖f - ∑ i ∈ s, lp.single p i (↑f i)‖ ^ p.toReal = ∑ i ∈ s, ‖↑f i‖ ^ p.toReal

Tactic:
refine ((hasSum_norm hp f).sub (hasSum_norm hp (f - ∑ i ∈ s, lp.single p i (f i)))).unique ?_

Result:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
hp : 0 < p.toReal
f : ↥(lp E p)
s : Finset α
⊢ HasSum (fun b => ‖↑f b‖ ^ p.toReal - ‖↑(f - ∑ i ∈ s, lp.single p i (↑f i)) b‖ ^ p.toReal) (∑ i ∈ s, ‖↑f i‖ ^ p.toReal)

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
hp : 0 < p.toReal
f : ↥(lp E p)
s : Finset α
F : α → ℝ := fun i => ‖↑f i‖ ^ p.toReal - ‖↑(f - ∑ i ∈ s, lp.single p i (↑f i)) i‖ ^ p.toReal
hF : ∀ i ∉ s, F i = 0
hF' : ∀ i ∈ s, F i = ‖↑f i‖ ^ p.toReal
this : HasSum F (∑ i ∈ s, F i)
⊢ HasSum (fun b => ‖↑f b‖ ^ p.toReal - ‖↑(f - ∑ i ∈ s, lp.single p i (↑f i)) b‖ ^ p.toReal) (∑ i ∈ s, ‖↑f i‖ ^ p.toReal)

Tactic:
rwa [Finset.sum_congr rfl hF'] at this

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/lpSpace.lean
theorem norm_zero : ‖(0 : lp E p)‖ = 0

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
⊢ ‖0‖ = 0

Tactic:
rcases p.trichotomy with (rfl | rfl | hp)

Result:
case inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
⊢ ‖0‖ = 0

case inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
⊢ ‖0‖ = 0

case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
⊢ ‖0‖ = 0

Proof state:
case inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
⊢ ‖0‖ = 0

Tactic:
simp [lp.norm_eq_ciSup]

Result:
no goals

Proof state:
case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
hp' : 1 / p.toReal ≠ 0
⊢ (∑' (i : α), ‖↑0 i‖ ^ p.toReal) ^ (1 / p.toReal) = 0

Tactic:
simpa [Real.zero_rpow hp.ne'] using Real.zero_rpow hp'

Result:
no goals

Proof state:
case inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
⊢ ‖0‖ = 0

Tactic:
simp [lp.norm_eq_card_dsupport]

Result:
no goals

Proof state:
case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
⊢ (∑' (i : α), ‖↑0 i‖ ^ p.toReal) ^ (1 / p.toReal) = 0

Tactic:
have hp' : 1 / p.toReal ≠ 0 := one_div_ne_zero hp.ne'

Result:
case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
hp' : 1 / p.toReal ≠ 0
⊢ (∑' (i : α), ‖↑0 i‖ ^ p.toReal) ^ (1 / p.toReal) = 0

Proof state:
case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
⊢ ‖0‖ = 0

Tactic:
rw [lp.norm_eq_tsum_rpow hp]

Result:
case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
⊢ (∑' (i : α), ‖↑0 i‖ ^ p.toReal) ^ (1 / p.toReal) = 0
-- Mathlib/AlgebraicGeometry/AffineSpace.lean
@[reassoc (attr := simp)]
lemma SpecIso_inv_over (R : CommRingCat.{max u v}) :
    (SpecIso n R).inv ≫ 𝔸(n; Spec R) ↘ Spec R = Spec.map (CommRingCat.ofHom C)

Proof state:
n : Type v
R : CommRingCat
⊢ (SpecIso n R).inv ≫ 𝔸(n; Spec R) ↘ Spec R = Spec.map (CommRingCat.ofHom C)

Tactic:
simp only [SpecIso, Iso.trans_inv, Functor.mapIso_inv, Iso.op_inv,
  mapEquiv_symm, RingEquiv.toRingHom_eq_coe, Scheme.Spec_map, Quiver.Hom.unop_op, Category.assoc,
  isoOfIsAffine_inv_over, Scheme.isoSpec_Spec_inv, ← Spec.map_comp]

Result:
n : Type v
R : CommRingCat
⊢ Spec.map
      ((Scheme.ΓSpecIso R).inv ≫
        CommRingCat.ofHom C ≫ (mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.inv) =
    Spec.map (CommRingCat.ofHom C)

Proof state:
case e_f
n : Type v
R : CommRingCat
⊢ CommRingCat.ofHom C ≫ (mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.inv =
    (Scheme.ΓSpecIso R).hom ≫ CommRingCat.ofHom C

Tactic:
ext : 2

Result:
case e_f.hf.a
n : Type v
R : CommRingCat
x✝ : ↑(CommRingCat.of ↑((Spec R).presheaf.toPrefunctor.1 (Opposite.op ⊤)))
⊢ (CommRingCat.Hom.hom
        (CommRingCat.ofHom C ≫ (mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.inv))
      x✝ =
    (CommRingCat.Hom.hom ((Scheme.ΓSpecIso R).hom ≫ CommRingCat.ofHom C)) x✝

Proof state:
n : Type v
R : CommRingCat
⊢ Spec.map
      ((Scheme.ΓSpecIso R).inv ≫
        CommRingCat.ofHom C ≫ (mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.inv) =
    Spec.map (CommRingCat.ofHom C)

Tactic:
congr 1

Result:
case e_f
n : Type v
R : CommRingCat
⊢ (Scheme.ΓSpecIso R).inv ≫
      CommRingCat.ofHom C ≫ (mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.inv =
    CommRingCat.ofHom C

Proof state:
case e_f
n : Type v
R : CommRingCat
⊢ (Scheme.ΓSpecIso R).inv ≫
      CommRingCat.ofHom C ≫ (mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.inv =
    CommRingCat.ofHom C

Tactic:
rw [Iso.inv_comp_eq]

Result:
case e_f
n : Type v
R : CommRingCat
⊢ CommRingCat.ofHom C ≫ (mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.inv =
    (Scheme.ΓSpecIso R).hom ≫ CommRingCat.ofHom C

Proof state:
case e_f.hf.a
n : Type v
R : CommRingCat
x✝ : ↑(CommRingCat.of ↑((Spec R).presheaf.toPrefunctor.1 (Opposite.op ⊤)))
⊢ (CommRingCat.Hom.hom
        (CommRingCat.ofHom C ≫ (mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.inv))
      x✝ =
    (CommRingCat.Hom.hom ((Scheme.ΓSpecIso R).hom ≫ CommRingCat.ofHom C)) x✝

Tactic:
exact map_C _ _

Result:
no goals
-- Mathlib/Analysis/Normed/Ring/Units.lean
theorem inverse_one_sub (t : R) (h : ‖t‖ < 1) : inverse (1 - t) = ↑(Units.oneSub t h)⁻¹

Proof state:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
t : R
h : ‖t‖ < 1
⊢ inverse (1 - t) = ↑(Units.oneSub t h)⁻¹

Tactic:
rw [← inverse_unit (Units.oneSub t h), Units.val_oneSub]

Result:
no goals
-- Mathlib/Data/Int/ModEq.lean
theorem neg (h : a ≡ b [ZMOD n]) : -a ≡ -b [ZMOD n] :=
  h.add_left_cancel (by simp_rw [← sub_eq_add_neg, sub_self]; rfl)

Proof state:
n a b : ℤ
h : a ≡ b [ZMOD n]
⊢ 0 ≡ 0 [ZMOD n]

Tactic:
rfl

Result:
no goals

Proof state:
n a b : ℤ
h : a ≡ b [ZMOD n]
⊢ a + -a ≡ b + -b [ZMOD n]

Tactic:
simp_rw [← sub_eq_add_neg, sub_self]

Result:
n a b : ℤ
h : a ≡ b [ZMOD n]
⊢ 0 ≡ 0 [ZMOD n]
-- Mathlib/FieldTheory/Isaacs.lean
theorem nonempty_algEquiv_of_range_minpoly_eq
    (h : Set.range (@minpoly F E _ _ _) = Set.range (@minpoly F K _ _ _)) :
    Nonempty (E ≃ₐ[F] K) :=
  have ⟨σ⟩ := nonempty_algHom_of_range_minpoly_subset h.le
  have : Algebra.IsAlgebraic F K := ⟨fun y ↦ IsIntegral.isAlgebraic <| by
    by_contra hy
    have ⟨x, hx⟩ := h.ge ⟨y, rfl⟩
    rw [minpoly.eq_zero hy] at hx
    exact minpoly.ne_zero ((alg.isIntegral).1 x) hx⟩
  have ⟨τ⟩ := nonempty_algHom_of_range_minpoly_subset h.ge
  ⟨.ofBijective _ (Algebra.IsAlgebraic.algHom_bijective₂ σ τ).1⟩

Proof state:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : Set.range (minpoly F) = Set.range (minpoly F)
σ : E →ₐ[F] K
y : K
⊢ IsIntegral F y

Tactic:
by_contra hy

Result:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : Set.range (minpoly F) = Set.range (minpoly F)
σ : E →ₐ[F] K
y : K
hy : ¬IsIntegral F y
⊢ False

Proof state:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : Set.range (minpoly F) = Set.range (minpoly F)
σ : E →ₐ[F] K
y : K
hy : ¬IsIntegral F y
x : E
hx : minpoly F x = 0
⊢ False

Tactic:
exact minpoly.ne_zero ((alg.isIntegral).1 x) hx

Result:
no goals

Proof state:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : Set.range (minpoly F) = Set.range (minpoly F)
σ : E →ₐ[F] K
y : K
hy : ¬IsIntegral F y
x : E
hx : minpoly F x = minpoly F y
⊢ False

Tactic:
rw [minpoly.eq_zero hy] at hx

Result:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : Set.range (minpoly F) = Set.range (minpoly F)
σ : E →ₐ[F] K
y : K
hy : ¬IsIntegral F y
x : E
hx : minpoly F x = 0
⊢ False

Proof state:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : Set.range (minpoly F) = Set.range (minpoly F)
σ : E →ₐ[F] K
y : K
hy : ¬IsIntegral F y
⊢ False

Tactic:
have ⟨x, hx⟩ := h.ge ⟨y, rfl⟩

Result:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : Set.range (minpoly F) = Set.range (minpoly F)
σ : E →ₐ[F] K
y : K
hy : ¬IsIntegral F y
x : E
hx : minpoly F x = minpoly F y
⊢ False
-- Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean
lemma quasiIso_map_iff_of_preservesLeftHomology
    [F.PreservesLeftHomologyOf S₁] [F.PreservesLeftHomologyOf S₂]
    [F.ReflectsIsomorphisms] :
    QuasiIso (F.mapShortComplex.map φ) ↔ QuasiIso φ

Proof state:
C : Type u_1
D : Type u_2
inst✝¹¹ : Category.{u_3, u_1} C
inst✝¹⁰ : Category.{u_4, u_2} D
inst✝⁹ : HasZeroMorphisms C
inst✝⁸ : HasZeroMorphisms D
F : C ⥤ D
inst✝⁷ : F.PreservesZeroMorphisms
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝⁶ : S₁.HasHomology
inst✝⁵ : S₂.HasHomology
inst✝⁴ : (F.mapShortComplex.obj S₁).HasHomology
inst✝³ : (F.mapShortComplex.obj S₂).HasHomology
inst✝² : F.PreservesLeftHomologyOf S₁
inst✝¹ : F.PreservesLeftHomologyOf S₂
inst✝ : F.ReflectsIsomorphisms
⊢ QuasiIso (F.mapShortComplex.map φ) ↔ QuasiIso φ

Tactic:
have γ : LeftHomologyMapData φ S₁.leftHomologyData S₂.leftHomologyData := default

Result:
C : Type u_1
D : Type u_2
inst✝¹¹ : Category.{u_3, u_1} C
inst✝¹⁰ : Category.{u_4, u_2} D
inst✝⁹ : HasZeroMorphisms C
inst✝⁸ : HasZeroMorphisms D
F : C ⥤ D
inst✝⁷ : F.PreservesZeroMorphisms
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝⁶ : S₁.HasHomology
inst✝⁵ : S₂.HasHomology
inst✝⁴ : (F.mapShortComplex.obj S₁).HasHomology
inst✝³ : (F.mapShortComplex.obj S₂).HasHomology
inst✝² : F.PreservesLeftHomologyOf S₁
inst✝¹ : F.PreservesLeftHomologyOf S₂
inst✝ : F.ReflectsIsomorphisms
γ : LeftHomologyMapData φ S₁.leftHomologyData S₂.leftHomologyData
⊢ QuasiIso (F.mapShortComplex.map φ) ↔ QuasiIso φ
-- Mathlib/Algebra/Group/Submonoid/Operations.lean
theorem map_mrange (g : N →* P) (f : M →* N) : f.mrange.map g = mrange (comp g f)

Proof state:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
g : N →* P
f : M →* N
⊢ map g (mrange f) = mrange (g.comp f)

Tactic:
simpa only [mrange_eq_map] using (⊤ : Submonoid M).map_map g f

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
protected lemma div_div_self (h : n ∣ m) (hm : m ≠ 0) : m / (m / n) = n

Proof state:
case intro
n w✝ : ℕ
hm : n * w✝ ≠ 0
⊢ n * w✝ / (n * w✝ / n) = n

Tactic:
rw [Nat.mul_ne_zero_iff] at hm

Result:
case intro
n w✝ : ℕ
hm : n ≠ 0 ∧ w✝ ≠ 0
⊢ n * w✝ / (n * w✝ / n) = n

Proof state:
m n : ℕ
h : n ∣ m
hm : m ≠ 0
⊢ m / (m / n) = n

Tactic:
rcases h with ⟨_, rfl⟩

Result:
case intro
n w✝ : ℕ
hm : n * w✝ ≠ 0
⊢ n * w✝ / (n * w✝ / n) = n

Proof state:
case intro
n w✝ : ℕ
hm : n ≠ 0 ∧ w✝ ≠ 0
⊢ n * w✝ / (n * w✝ / n) = n

Tactic:
rw [mul_div_right _ (Nat.pos_of_ne_zero hm.1), mul_div_left _ (Nat.pos_of_ne_zero hm.2)]

Result:
no goals
-- Mathlib/Data/Set/Basic.lean
theorem subset_ite {t s s' u : Set α} : u ⊆ t.ite s s' ↔ u ∩ t ⊆ s ∧ u \ t ⊆ s'

Proof state:
α : Type u
t s s' u : Set α
⊢ u ⊆ t.ite s s' ↔ u ∩ t ⊆ s ∧ u \ t ⊆ s'

Tactic:
simp only [subset_def, ← forall_and]

Result:
α : Type u
t s s' u : Set α
⊢ (∀ x ∈ u, x ∈ t.ite s s') ↔ ∀ (x : α), (x ∈ u ∩ t → x ∈ s) ∧ (x ∈ u \ t → x ∈ s')

Proof state:
α : Type u
t s s' u : Set α
⊢ (∀ x ∈ u, x ∈ t.ite s s') ↔ ∀ (x : α), (x ∈ u ∩ t → x ∈ s) ∧ (x ∈ u \ t → x ∈ s')

Tactic:
refine forall_congr' fun x => ?_

Result:
α : Type u
t s s' u : Set α
x : α
⊢ x ∈ u → x ∈ t.ite s s' ↔ (x ∈ u ∩ t → x ∈ s) ∧ (x ∈ u \ t → x ∈ s')

Proof state:
α : Type u
t s s' u : Set α
x : α
⊢ x ∈ u → x ∈ t.ite s s' ↔ (x ∈ u ∩ t → x ∈ s) ∧ (x ∈ u \ t → x ∈ s')

Tactic:
by_cases hx : x ∈ t <;> simp [*, Set.ite]

Result:
no goals