harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean
@[reassoc]
lemma naturality_δ (f : S₁ ⟶ S₂) : S₁.δ ≫ f.f₃.τ₁ = f.f₀.τ₃ ≫ S₂.δ

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S₁ S₂ : SnakeInput C
f : S₁ ⟶ S₂
⊢ S₁.δ ≫ f.f₃.τ₁ = f.f₀.τ₃ ≫ S₂.δ

Tactic:
rw [← cancel_epi (pullback.snd _ _ : S₁.P ⟶ _), S₁.snd_δ_assoc, ← comp_τ₁, ← f.comm₂₃,
  comp_τ₁, naturality_φ₁_assoc, ← S₂.snd_δ, functorP_map, pullback.lift_snd_assoc, assoc]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/List/Basic.lean
theorem tail_sum (L : List ℕ) : L.tail.sum = L.sum - L.headI

Proof state:
L : List ℕ
⊢ L.tail.sum = L.sum - L.headI

Tactic:
rw [← headI_add_tail_sum L, add_comm, Nat.add_sub_cancel_right]

Result:
no goals
-- Mathlib/Algebra/Lie/Subalgebra.lean
theorem sInf_glb (S : Set (LieSubalgebra R L)) : IsGLB S (sInf S)

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
S : Set (LieSubalgebra R L)
h : ∀ (K K' : LieSubalgebra R L), ↑K ≤ ↑K' ↔ K ≤ K'
⊢ IsGLB S (sInf S)

Tactic:
apply IsGLB.of_image @h

Result:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
S : Set (LieSubalgebra R L)
h : ∀ (K K' : LieSubalgebra R L), ↑K ≤ ↑K' ↔ K ≤ K'
⊢ IsGLB (SetLike.coe '' S) ↑(sInf S)

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
S : Set (LieSubalgebra R L)
⊢ IsGLB S (sInf S)

Tactic:
have h : ∀ K K' : LieSubalgebra R L, (K : Set L) ≤ K' ↔ K ≤ K' := by
  intros
  exact Iff.rfl

Result:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
S : Set (LieSubalgebra R L)
h : ∀ (K K' : LieSubalgebra R L), ↑K ≤ ↑K' ↔ K ≤ K'
⊢ IsGLB S (sInf S)

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
S : Set (LieSubalgebra R L)
h : ∀ (K K' : LieSubalgebra R L), ↑K ≤ ↑K' ↔ K ≤ K'
⊢ IsGLB (SetLike.coe '' S) ↑(sInf S)

Tactic:
simp only [sInf_coe]

Result:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
S : Set (LieSubalgebra R L)
h : ∀ (K K' : LieSubalgebra R L), ↑K ≤ ↑K' ↔ K ≤ K'
⊢ IsGLB (SetLike.coe '' S) (⋂ s ∈ S, ↑s)

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
S : Set (LieSubalgebra R L)
K✝ K'✝ : LieSubalgebra R L
⊢ ↑K✝ ≤ ↑K'✝ ↔ K✝ ≤ K'✝

Tactic:
exact Iff.rfl

Result:
no goals

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
S : Set (LieSubalgebra R L)
⊢ ∀ (K K' : LieSubalgebra R L), ↑K ≤ ↑K' ↔ K ≤ K'

Tactic:
intros

Result:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
S : Set (LieSubalgebra R L)
K✝ K'✝ : LieSubalgebra R L
⊢ ↑K✝ ≤ ↑K'✝ ↔ K✝ ≤ K'✝

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
S : Set (LieSubalgebra R L)
h : ∀ (K K' : LieSubalgebra R L), ↑K ≤ ↑K' ↔ K ≤ K'
⊢ IsGLB (SetLike.coe '' S) (⋂ s ∈ S, ↑s)

Tactic:
exact isGLB_biInf

Result:
no goals
-- Mathlib/Algebra/CharP/Defs.lean
/-- The exponential characteristic is positive. -/
lemma expChar_pos (q : ℕ) [ExpChar R q] : 0 < q

Proof state:
R : Type u_1
inst✝¹ : AddMonoidWithOne R
q : ℕ
inst✝ : ExpChar R q
⊢ 0 < q

Tactic:
rcases expChar_is_prime_or_one R q with h | rfl

Result:
case inl
R : Type u_1
inst✝¹ : AddMonoidWithOne R
q : ℕ
inst✝ : ExpChar R q
h : Nat.Prime q
⊢ 0 < q

case inr
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : ExpChar R 1
⊢ 0 < 1

Proof state:
case inl
R : Type u_1
inst✝¹ : AddMonoidWithOne R
q : ℕ
inst✝ : ExpChar R q
h : Nat.Prime q
⊢ 0 < q

case inr
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : ExpChar R 1
⊢ 0 < 1

Tactic:
exacts [Nat.Prime.pos h, Nat.one_pos]

Result:
no goals
-- Mathlib/Analysis/Normed/Ring/SeminormFromBounded.lean
theorem seminormFromBounded_bddAbove_range (f_nonneg : 0 ≤ f)
    (f_mul : ∀ x y : R, f (x * y) ≤ c * f x * f y) (x : R) :
    BddAbove (Set.range fun y ↦ f (x * y) / f y)

Proof state:
case h.intro.inl
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x y : R
hy0 : f y = 0 y
⊢ (fun y => f (x * y) / f y) y ≤ c * f x

Tactic:
simpa [hy0] using seminormFromBounded_aux f_nonneg f_mul x

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
⊢ BddAbove (Set.range fun y => f (x * y) / f y)

Tactic:
use c * f x

Result:
case h
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
⊢ c * f x ∈ upperBounds (Set.range fun y => f (x * y) / f y)

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
⊢ c * f x ∈ upperBounds (Set.range fun y => f (x * y) / f y)

Tactic:
rintro r ⟨y, rfl⟩

Result:
case h.intro
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x y : R
⊢ (fun y => f (x * y) / f y) y ≤ c * f x

Proof state:
case h.intro.inr
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x y : R
hy0 : 0 y < f y
⊢ (fun y => f (x * y) / f y) y ≤ c * f x

Tactic:
simpa [div_le_iff₀ hy0] using f_mul x y

Result:
no goals

Proof state:
case h.intro
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x y : R
⊢ (fun y => f (x * y) / f y) y ≤ c * f x

Tactic:
rcases (f_nonneg y).eq_or_gt with hy0 | hy0

Result:
case h.intro.inl
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x y : R
hy0 : f y = 0 y
⊢ (fun y => f (x * y) / f y) y ≤ c * f x

case h.intro.inr
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x y : R
hy0 : 0 y < f y
⊢ (fun y => f (x * y) / f y) y ≤ c * f x
-- Mathlib/Analysis/Normed/Group/HomCompletion.lean
theorem NormedAddGroupHom.extension_unique (f : NormedAddGroupHom G H)
    {g : NormedAddGroupHom (Completion G) H} (hg : ∀ v, f v = g v) : f.extension = g

Proof state:
G : Type u_1
inst✝³ : SeminormedAddCommGroup G
H : Type u_2
inst✝² : SeminormedAddCommGroup H
inst✝¹ : T0Space H
inst✝ : CompleteSpace H
f : NormedAddGroupHom G H
g : NormedAddGroupHom (Completion G) H
hg : ∀ (v : G), f v = g ↑v
⊢ f.extension = g

Tactic:
ext v

Result:
case H
G : Type u_1
inst✝³ : SeminormedAddCommGroup G
H : Type u_2
inst✝² : SeminormedAddCommGroup H
inst✝¹ : T0Space H
inst✝ : CompleteSpace H
f : NormedAddGroupHom G H
g : NormedAddGroupHom (Completion G) H
hg : ∀ (v : G), f v = g ↑v
v : Completion G
⊢ f.extension v = g v

Proof state:
case H
G : Type u_1
inst✝³ : SeminormedAddCommGroup G
H : Type u_2
inst✝² : SeminormedAddCommGroup H
inst✝¹ : T0Space H
inst✝ : CompleteSpace H
f : NormedAddGroupHom G H
g : NormedAddGroupHom (Completion G) H
hg : ∀ (v : G), f v = g ↑v
v : Completion G
⊢ f.extension v = g v

Tactic:
rw [NormedAddGroupHom.extension_coe_to_fun,
  Completion.extension_unique f.uniformContinuous g.uniformContinuous fun a => hg a]

Result:
no goals
-- Mathlib/Topology/Separation/Basic.lean
theorem Set.Finite.continuousOn [T1Space X] [TopologicalSpace Y] {s : Set X} (hs : s.Finite)
    (f : X → Y) : ContinuousOn f s

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : TopologicalSpace Y
s : Set X
hs : s.Finite
f : X → Y
⊢ ContinuousOn f s

Tactic:
rw [continuousOn_iff_continuous_restrict]

Result:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : TopologicalSpace Y
s : Set X
hs : s.Finite
f : X → Y
⊢ Continuous (s.restrict f)

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : TopologicalSpace Y
s : Set X
hs : s.Finite
f : X → Y
⊢ Continuous (s.restrict f)

Tactic:
have : Finite s := hs

Result:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : TopologicalSpace Y
s : Set X
hs : s.Finite
f : X → Y
this : Finite ↑s
⊢ Continuous (s.restrict f)

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : TopologicalSpace Y
s : Set X
hs : s.Finite
f : X → Y
this : Finite ↑s
⊢ Continuous (s.restrict f)

Tactic:
fun_prop

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem enumFrom_eq_append_iff {l : List α} {n : Nat} :
    l.enumFrom n = l₁ ++ l₂ ↔
      ∃ l₁' l₂', l = l₁' ++ l₂' ∧ l₁ = l₁'.enumFrom n ∧ l₂ = l₂'.enumFrom (n + l₁'.length)

Proof state:
case mpr.intro.intro.intro.intro
α : Type u_1
n : Nat
l₁' l₂' : List α
⊢ ∃ w x y z,
    w.length = y.length ∧
      range' n (l₁' ++ l₂').length = w ++ x ∧
        l₁' ++ l₂' = y ++ z ∧ enumFrom n l₁' = w.zip y ∧ enumFrom (n + l₁'.length) l₂' = x.zip z

Tactic:
simp only [enumFrom_eq_zip_range']

Result:
case mpr.intro.intro.intro.intro
α : Type u_1
n : Nat
l₁' l₂' : List α
⊢ ∃ w x y z,
    w.length = y.length ∧
      range' n (l₁' ++ l₂').length = w ++ x ∧
        l₁' ++ l₂' = y ++ z ∧
          (range' n l₁'.length).zip l₁' = w.zip y ∧ (range' (n + l₁'.length) l₂'.length).zip l₂' = x.zip z

Proof state:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.e_a.e_len
α : Type u_1
n : Nat
y z : List α
⊢ y.length + z.length - y.length = z.length

Tactic:
omega

Result:
no goals

Proof state:
case mpr.intro.intro.intro.intro
α : Type u_1
n : Nat
l₁' l₂' : List α
⊢ ∃ w x y z,
    w.length = y.length ∧
      range' n (l₁' ++ l₂').length = w ++ x ∧
        l₁' ++ l₂' = y ++ z ∧
          (range' n l₁'.length).zip l₁' = w.zip y ∧ (range' (n + l₁'.length) l₂'.length).zip l₂' = x.zip z

Tactic:
refine ⟨range' n l₁'.length, range' (n + l₁'.length) l₂'.length, l₁', l₂', ?_⟩

Result:
case mpr.intro.intro.intro.intro
α : Type u_1
n : Nat
l₁' l₂' : List α
⊢ (range' n l₁'.length).length = l₁'.length ∧
    range' n (l₁' ++ l₂').length = range' n l₁'.length ++ range' (n + l₁'.length) l₂'.length ∧
      l₁' ++ l₂' = l₁' ++ l₂' ∧
        (range' n l₁'.length).zip l₁' = (range' n l₁'.length).zip l₁' ∧
          (range' (n + l₁'.length) l₂'.length).zip l₂' = (range' (n + l₁'.length) l₂'.length).zip l₂'
-- Mathlib/Order/Filter/AtTopBot/Basic.lean
theorem eventually_forall_ge_atTop [Preorder α] {p : α → Prop} :
    (∀ᶠ x in atTop, ∀ y, x ≤ y → p y) ↔ ∀ᶠ x in atTop, p x

Proof state:
case intro.intro
α : Type u_3
inst✝ : Preorder α
p : α → Prop
h : ∀ᶠ (x : α) in atTop, p x
S : Set α
hSf : S.Finite
hS : ∀ ⦃x : α⦄, x ∈ ⋂ i ∈ S, Ici i → p x
x : α
hx : x ∈ ⋂ i, (fun x => Ici ↑x) i
y : α
hy : x ≤ y
⊢ p y

Tactic:
simp only [mem_iInter] at hS hx

Result:
case intro.intro
α : Type u_3
inst✝ : Preorder α
p : α → Prop
h : ∀ᶠ (x : α) in atTop, p x
S : Set α
hSf : S.Finite
x y : α
hy : x ≤ y
hS : ∀ ⦃x : α⦄, (∀ i ∈ S, x ∈ Ici i) → p x
hx : ∀ (i : ↑S), x ∈ Ici ↑i
⊢ p y

Proof state:
case intro.intro
α : Type u_3
inst✝ : Preorder α
p : α → Prop
h : ∀ᶠ (x : α) in atTop, p x
S : Set α
hSf : S.Finite
hS : ∀ ⦃x : α⦄, x ∈ ⋂ i ∈ S, Ici i → p x
⊢ ∀ᶠ (x : α) in atTop, ∀ (y : α), x ≤ y → p y

Tactic:
refine mem_iInf_of_iInter hSf (V := fun x ↦ Ici x.1) (fun _ ↦ Subset.rfl) fun x hx y hy ↦ ?_

Result:
case intro.intro
α : Type u_3
inst✝ : Preorder α
p : α → Prop
h : ∀ᶠ (x : α) in atTop, p x
S : Set α
hSf : S.Finite
hS : ∀ ⦃x : α⦄, x ∈ ⋂ i ∈ S, Ici i → p x
x : α
hx : x ∈ ⋂ i, (fun x => Ici ↑x) i
y : α
hy : x ≤ y
⊢ p y

Proof state:
α : Type u_3
inst✝ : Preorder α
p : α → Prop
⊢ (∀ᶠ (x : α) in atTop, ∀ (y : α), x ≤ y → p y) ↔ ∀ᶠ (x : α) in atTop, p x

Tactic:
refine ⟨fun h ↦ h.mono fun x hx ↦ hx x le_rfl, fun h ↦ ?_⟩

Result:
α : Type u_3
inst✝ : Preorder α
p : α → Prop
h : ∀ᶠ (x : α) in atTop, p x
⊢ ∀ᶠ (x : α) in atTop, ∀ (y : α), x ≤ y → p y

Proof state:
case intro.intro
α : Type u_3
inst✝ : Preorder α
p : α → Prop
h : ∀ᶠ (x : α) in atTop, p x
S : Set α
hSf : S.Finite
x y : α
hy : x ≤ y
hS : ∀ ⦃x : α⦄, (∀ i ∈ S, x ∈ Ici i) → p x
hx : ∀ (i : ↑S), x ∈ Ici ↑i
⊢ p y

Tactic:
exact hS fun z hz ↦ le_trans (hx ⟨z, hz⟩) hy

Result:
no goals

Proof state:
α : Type u_3
inst✝ : Preorder α
p : α → Prop
h : ∀ᶠ (x : α) in atTop, p x
⊢ ∀ᶠ (x : α) in atTop, ∀ (y : α), x ≤ y → p y

Tactic:
rcases (hasBasis_iInf_principal_finite _).eventually_iff.1 h with ⟨S, hSf, hS⟩

Result:
case intro.intro
α : Type u_3
inst✝ : Preorder α
p : α → Prop
h : ∀ᶠ (x : α) in atTop, p x
S : Set α
hSf : S.Finite
hS : ∀ ⦃x : α⦄, x ∈ ⋂ i ∈ S, Ici i → p x
⊢ ∀ᶠ (x : α) in atTop, ∀ (y : α), x ≤ y → p y
-- Mathlib/FieldTheory/RatFunc/Defs.lean
theorem toFractionRing_injective : Function.Injective (toFractionRing : _ → FractionRing K[X])
  | ⟨x⟩, ⟨y⟩, xy => by subst xy; rfl

Proof state:
K : Type u
inst✝ : CommRing K
x y : FractionRing K[X]
xy : { toFractionRing := x }.toFractionRing = { toFractionRing := y }.toFractionRing
⊢ { toFractionRing := x } = { toFractionRing := y }

Tactic:
subst xy

Result:
K : Type u
inst✝ : CommRing K
x : FractionRing K[X]
⊢ { toFractionRing := x } = { toFractionRing := { toFractionRing := x }.toFractionRing }

Proof state:
K : Type u
inst✝ : CommRing K
x : FractionRing K[X]
⊢ { toFractionRing := x } = { toFractionRing := { toFractionRing := x }.toFractionRing }

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/Lattice.lean
theorem semilatticeSup_mk'_partialOrder_eq_semilatticeInf_mk'_partialOrder
    {α : Type*} [Max α] [Min α]
    (sup_comm : ∀ a b : α, a ⊔ b = b ⊔ a) (sup_assoc : ∀ a b c : α, a ⊔ b ⊔ c = a ⊔ (b ⊔ c))
    (sup_idem : ∀ a : α, a ⊔ a = a) (inf_comm : ∀ a b : α, a ⊓ b = b ⊓ a)
    (inf_assoc : ∀ a b c : α, a ⊓ b ⊓ c = a ⊓ (b ⊓ c)) (inf_idem : ∀ a : α, a ⊓ a = a)
    (sup_inf_self : ∀ a b : α, a ⊔ a ⊓ b = a) (inf_sup_self : ∀ a b : α, a ⊓ (a ⊔ b) = a) :
    @SemilatticeSup.toPartialOrder _ (SemilatticeSup.mk' sup_comm sup_assoc sup_idem) =
      @SemilatticeInf.toPartialOrder _ (SemilatticeInf.mk' inf_comm inf_assoc inf_idem) :=
  PartialOrder.ext fun a b =>
    show a ⊔ b = b ↔ b ⊓ a = a from
      ⟨fun h => by rw [← h, inf_comm, inf_sup_self], fun h => by rw [← h, sup_comm, sup_inf_self]⟩

Proof state:
α : Type u_1
inst✝¹ : Max α
inst✝ : Min α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
sup_idem : ∀ (a : α), a ⊔ a = a
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
inf_idem : ∀ (a : α), a ⊓ a = a
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
a b : α
h : a ⊔ b = b
⊢ b ⊓ a = a

Tactic:
rw [← h, inf_comm, inf_sup_self]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Max α
inst✝ : Min α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
sup_idem : ∀ (a : α), a ⊔ a = a
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
inf_idem : ∀ (a : α), a ⊓ a = a
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
a b : α
h : b ⊓ a = a
⊢ a ⊔ b = b

Tactic:
rw [← h, sup_comm, sup_inf_self]

Result:
no goals
-- Mathlib/Algebra/Group/Units/Defs.lean
@[to_additive] lemma div (ha : IsUnit a) (hb : IsUnit b) : IsUnit (a / b)

Proof state:
α : Type u
inst✝ : DivisionMonoid α
a b : α
ha : IsUnit a
hb : IsUnit b
⊢ IsUnit (a / b)

Tactic:
rw [div_eq_mul_inv]

Result:
α : Type u
inst✝ : DivisionMonoid α
a b : α
ha : IsUnit a
hb : IsUnit b
⊢ IsUnit (a * b⁻¹)

Proof state:
α : Type u
inst✝ : DivisionMonoid α
a b : α
ha : IsUnit a
hb : IsUnit b
⊢ IsUnit (a * b⁻¹)

Tactic:
exact ha.mul hb.inv

Result:
no goals
-- Mathlib/SetTheory/Surreal/Basic.lean
theorem insertRight_numeric {x x' : PGame} (x_num : x.Numeric) (x'_num : x'.Numeric)
    (h : x ≤ x') : (insertRight x x').Numeric

Proof state:
x x' : PGame
x_num : x.Numeric
x'_num : x'.Numeric
h : x ≤ x'
⊢ (-(-x).insertLeft (-x')).Numeric

Tactic:
apply Numeric.neg

Result:
case x
x x' : PGame
x_num : x.Numeric
x'_num : x'.Numeric
h : x ≤ x'
⊢ ((-x).insertLeft (-x')).Numeric

Proof state:
case x
x x' : PGame
x_num : x.Numeric
x'_num : x'.Numeric
h : x ≤ x'
⊢ ((-x).insertLeft (-x')).Numeric

Tactic:
exact insertLeft_numeric (Numeric.neg x_num) (Numeric.neg x'_num) (neg_le_neg_iff.mpr h)

Result:
no goals

Proof state:
x x' : PGame
x_num : x.Numeric
x'_num : x'.Numeric
h : x ≤ x'
⊢ (x.insertRight x').Numeric

Tactic:
rw [← neg_neg (x.insertRight x'), ← neg_insertLeft_neg]

Result:
x x' : PGame
x_num : x.Numeric
x'_num : x'.Numeric
h : x ≤ x'
⊢ (-(-x).insertLeft (-x')).Numeric
-- Mathlib/GroupTheory/FreeGroup/Basic.lean
theorem lift.range_eq_closure : (lift f).range = Subgroup.closure (Set.range f)

Proof state:
α : Type u
β : Type v
inst✝ : Group β
f : α → β
⊢ Set.range f ⊆ ↑(lift f).range

Tactic:
rintro _ ⟨a, rfl⟩

Result:
case intro
α : Type u
β : Type v
inst✝ : Group β
f : α → β
a : α
⊢ f a ∈ ↑(lift f).range

Proof state:
case intro
α : Type u
β : Type v
inst✝ : Group β
f : α → β
a : α
⊢ f a ∈ ↑(lift f).range

Tactic:
exact ⟨FreeGroup.of a, by simp only [lift.of]⟩

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝ : Group β
f : α → β
⊢ (lift f).range = Subgroup.closure (Set.range f)

Tactic:
apply le_antisymm (lift.range_le Subgroup.subset_closure)

Result:
α : Type u
β : Type v
inst✝ : Group β
f : α → β
⊢ Subgroup.closure (Set.range f) ≤ (lift f).range

Proof state:
α : Type u
β : Type v
inst✝ : Group β
f : α → β
a : α
⊢ (lift f) (FreeGroup.of a) = f a

Tactic:
simp only [lift.of]

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝ : Group β
f : α → β
⊢ Subgroup.closure (Set.range f) ≤ (lift f).range

Tactic:
rw [Subgroup.closure_le]

Result:
α : Type u
β : Type v
inst✝ : Group β
f : α → β
⊢ Set.range f ⊆ ↑(lift f).range
-- Mathlib/RingTheory/Ideal/Quotient/Operations.lean
lemma Quotient.mk_bijective_iff_eq_bot (I : Ideal A) [I.IsTwoSided] :
    Function.Bijective (mk I) ↔ I = ⊥

Proof state:
case mp
A : Type u_3
inst✝¹ : Ring A
I : Ideal A
inst✝ : I.IsTwoSided
h : Bijective ⇑(mk I)
⊢ map (mk I) I = ⊥

Tactic:
exact (map_eq_bot_iff_le_ker _).mpr <| le_of_eq mk_ker.symm

Result:
no goals

Proof state:
case mpr
A : Type u_3
inst✝¹ : Ring A
I : Ideal A
inst✝ : I.IsTwoSided
⊢ I = ⊥ → Bijective ⇑(mk I)

Tactic:
exact fun h => ⟨(injective_iff_ker_eq_bot _).mpr <| by rw [mk_ker, h], mk_surjective⟩

Result:
no goals

Proof state:
case mp
A : Type u_3
inst✝¹ : Ring A
I : Ideal A
inst✝ : I.IsTwoSided
h : Bijective ⇑(mk I)
⊢ I = ⊥

Tactic:
rw [← map_eq_bot_iff_of_injective h.1]

Result:
case mp
A : Type u_3
inst✝¹ : Ring A
I : Ideal A
inst✝ : I.IsTwoSided
h : Bijective ⇑(mk I)
⊢ map (mk I) I = ⊥

Proof state:
case mp
A : Type u_3
inst✝¹ : Ring A
I : Ideal A
inst✝ : I.IsTwoSided
⊢ Bijective ⇑(mk I) → I = ⊥

Tactic:
intro h

Result:
case mp
A : Type u_3
inst✝¹ : Ring A
I : Ideal A
inst✝ : I.IsTwoSided
h : Bijective ⇑(mk I)
⊢ I = ⊥

Proof state:
A : Type u_3
inst✝¹ : Ring A
I : Ideal A
inst✝ : I.IsTwoSided
⊢ Bijective ⇑(mk I) ↔ I = ⊥

Tactic:
constructor

Result:
case mp
A : Type u_3
inst✝¹ : Ring A
I : Ideal A
inst✝ : I.IsTwoSided
⊢ Bijective ⇑(mk I) → I = ⊥

case mpr
A : Type u_3
inst✝¹ : Ring A
I : Ideal A
inst✝ : I.IsTwoSided
⊢ I = ⊥ → Bijective ⇑(mk I)

Proof state:
A : Type u_3
inst✝¹ : Ring A
I : Ideal A
inst✝ : I.IsTwoSided
h : I = ⊥
⊢ ker (mk I) = ⊥

Tactic:
rw [mk_ker, h]

Result:
no goals
-- Mathlib/Data/Finset/Powerset.lean
theorem coe_powerset (s : Finset α) :
    (s.powerset : Set (Finset α)) = ((↑) : Finset α → Set α) ⁻¹' (s : Set α).powerset

Proof state:
α : Type u_1
s : Finset α
⊢ ↑s.powerset = toSet ⁻¹' 𝒫↑s

Tactic:
ext

Result:
case h
α : Type u_1
s x✝ : Finset α
⊢ x✝ ∈ ↑s.powerset ↔ x✝ ∈ toSet ⁻¹' 𝒫↑s

Proof state:
case h
α : Type u_1
s x✝ : Finset α
⊢ x✝ ∈ ↑s.powerset ↔ x✝ ∈ toSet ⁻¹' 𝒫↑s

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/NeZero.lean
theorem inv_mul_cancel₀ (h : a ≠ 0) : a⁻¹ * a = 1 :=
  calc
    a⁻¹ * a = a⁻¹ * a * a⁻¹ * a⁻¹⁻¹

Proof state:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
h : a ≠ 0
⊢ a⁻¹ * a * a⁻¹ * a⁻¹⁻¹ = a⁻¹ * a⁻¹⁻¹

Tactic:
simp [h]

Result:
no goals

Proof state:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
h : a ≠ 0
⊢ a⁻¹ * a⁻¹⁻¹ = 1

Tactic:
simp [inv_ne_zero h]

Result:
no goals

Proof state:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
h : a ≠ 0
⊢ a⁻¹ * a = a⁻¹ * a * a⁻¹ * a⁻¹⁻¹

Tactic:
simp [inv_ne_zero h]

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

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

Tactic:
simp only [reduceOption, filterMap, id]

Result:
no goals
-- Mathlib/Topology/Maps/Basic.lean
theorem isOpen_range (hf : IsOpenMap f) : IsOpen (range f)

Proof state:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenMap f
⊢ IsOpen (range f)

Tactic:
rw [← image_univ]

Result:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenMap f
⊢ IsOpen (f '' univ)

Proof state:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenMap f
⊢ IsOpen (f '' univ)

Tactic:
exact hf _ isOpen_univ

Result:
no goals
-- Mathlib/Data/Nat/Nth.lean
lemma nth_add {m n : ℕ} (h0 : ∀ k < m, ¬p k) (h : nth p n ≠ 0) :
    nth (fun i ↦ p (i + m)) n + m = nth p n

Proof state:
p : ℕ → Prop
m n : ℕ
h0 : ∀ k < m, ¬p k
h : nth p n ≠ 0
k : ℕ
hk : p k
hn : k ∉ Set.range fun x => id x + m
⊢ False

Tactic:
simp_rw [id_eq, Set.mem_range, eq_comm] at hn

Result:
p : ℕ → Prop
m n : ℕ
h0 : ∀ k < m, ¬p k
h : nth p n ≠ 0
k : ℕ
hk : p k
hn : ¬∃ y, k = y + m
⊢ False

Proof state:
p : ℕ → Prop
m n : ℕ
h0 : ∀ k < m, ¬p k
h : nth p n ≠ 0
⊢ nth (fun i => p (i + m)) n + m = nth p n

Tactic:
refine nth_comp_of_strictMono (strictMono_id.add_const m) (fun k hk ↦ ?_)
  (fun hf ↦ lt_card_toFinset_of_nth_ne_zero h hf)

Result:
p : ℕ → Prop
m n : ℕ
h0 : ∀ k < m, ¬p k
h : nth p n ≠ 0
k : ℕ
hk : p k
⊢ k ∈ Set.range fun x => id x + m

Proof state:
p : ℕ → Prop
m n : ℕ
h0 : ∀ k < m, ¬p k
h : nth p n ≠ 0
k : ℕ
hk : p k
hn : ¬∃ y, k = y + m
⊢ False

Tactic:
exact h0 _ (not_le.mp fun h ↦ hn (le_iff_exists_add'.mp h)) hk

Result:
no goals

Proof state:
p : ℕ → Prop
m n : ℕ
h0 : ∀ k < m, ¬p k
h : nth p n ≠ 0
k : ℕ
hk : p k
⊢ k ∈ Set.range fun x => id x + m

Tactic:
by_contra hn

Result:
p : ℕ → Prop
m n : ℕ
h0 : ∀ k < m, ¬p k
h : nth p n ≠ 0
k : ℕ
hk : p k
hn : k ∉ Set.range fun x => id x + m
⊢ False
-- Mathlib/Algebra/Polynomial/Reverse.lean
theorem coeff_reflect (N : ℕ) (f : R[X]) (i : ℕ) : coeff (reflect N f) i = f.coeff (revAt N i)

Proof state:
case ofFinsupp
R : Type u_1
inst✝ : Semiring R
N i : ℕ
f : AddMonoidAlgebra R ℕ
⊢ (embDomain (revAt N) f) i = f ((revAt N) i)

Tactic:
calc
  Finsupp.embDomain (revAt N) f i = Finsupp.embDomain (revAt N) f (revAt N (revAt N i)) := by
    rw [revAt_invol]
  _ = f (revAt N i) := Finsupp.embDomain_apply _ _ _

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
N : ℕ
f : R[X]
i : ℕ
⊢ (reflect N f).coeff i = f.coeff ((revAt N) i)

Tactic:
rcases f with ⟨f⟩

Result:
case ofFinsupp
R : Type u_1
inst✝ : Semiring R
N i : ℕ
f : AddMonoidAlgebra R ℕ
⊢ (reflect N { toFinsupp := f }).coeff i = { toFinsupp := f }.coeff ((revAt N) i)

Proof state:
R : Type u_1
inst✝ : Semiring R
N i : ℕ
f : AddMonoidAlgebra R ℕ
⊢ (embDomain (revAt N) f) i = (embDomain (revAt N) f) ((revAt N) ((revAt N) i))

Tactic:
rw [revAt_invol]

Result:
no goals

Proof state:
case ofFinsupp
R : Type u_1
inst✝ : Semiring R
N i : ℕ
f : AddMonoidAlgebra R ℕ
⊢ (reflect N { toFinsupp := f }).coeff i = { toFinsupp := f }.coeff ((revAt N) i)

Tactic:
simp only [reflect, coeff]

Result:
case ofFinsupp
R : Type u_1
inst✝ : Semiring R
N i : ℕ
f : AddMonoidAlgebra R ℕ
⊢ (embDomain (revAt N) f) i = f ((revAt N) i)