harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/SetTheory/Surreal/Multiplication.lean
/-- That the left options of `x * y` are less than itself and the right options are greater, which
  is part of the condition that `x * y` is numeric, is equivalent to the conjunction of various
  `MulOptionsLTMul` statements for `x`, `y` and their negations. We only show the forward
  direction. -/
lemma mulOptionsLTMul_of_numeric (hn : (x * y).Numeric) :
    (MulOptionsLTMul x y ∧ MulOptionsLTMul (-x) (-y)) ∧
    (MulOptionsLTMul x (-y) ∧ MulOptionsLTMul (-x) y)

Proof state:
case right.refine_2
x y : PGame
hn : (x * y).Numeric
h :
  (∀ (i : x.LeftMoves) (j : (-y).LeftMoves), ⟦x * y⟧ < -⟦x.mulOption (-y) i j⟧) ∧
    ∀ (i : (-x).LeftMoves) (j : y.LeftMoves), ⟦x * y⟧ < -⟦(-x).mulOption y i j⟧
a : (-x).LeftMoves
b : y.LeftMoves
⊢ ⟦x * y⟧ < -⟦(-x).mulOption y a b⟧ → ⟦(-x).mulOption y a b⟧ < ⟦-x * y⟧

Tactic:
rw [lt_neg]

Result:
case right.refine_2
x y : PGame
hn : (x * y).Numeric
h :
  (∀ (i : x.LeftMoves) (j : (-y).LeftMoves), ⟦x * y⟧ < -⟦x.mulOption (-y) i j⟧) ∧
    ∀ (i : (-x).LeftMoves) (j : y.LeftMoves), ⟦x * y⟧ < -⟦(-x).mulOption y i j⟧
a : (-x).LeftMoves
b : y.LeftMoves
⊢ ⟦(-x).mulOption y a b⟧ < -⟦x * y⟧ → ⟦(-x).mulOption y a b⟧ < ⟦-x * y⟧

Proof state:
case left
x y : PGame
hn : (x * y).Numeric
h : ∀ (i : (x * y).LeftMoves), ⟦(x * y).moveLeft i⟧ < ⟦x * y⟧
⊢ MulOptionsLTMul x y ∧ MulOptionsLTMul (-x) (-y)

Tactic:
convert (leftMoves_mul_iff <| GT.gt _).1 h

Result:
case h.e'_2.a
x y : PGame
hn : (x * y).Numeric
h : ∀ (i : (x * y).LeftMoves), ⟦(x * y).moveLeft i⟧ < ⟦x * y⟧
⊢ MulOptionsLTMul (-x) (-y) ↔ ∀ (i : (-x).LeftMoves) (j : (-y).LeftMoves), ⟦x * y⟧ > ⟦(-x).mulOption (-y) i j⟧
-- Mathlib/CategoryTheory/Iso.lean
theorem of_isIso_comp_right {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso g] [IsIso (f ≫ g)] :
    IsIso f

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsIso g
inst✝ : IsIso (f ≫ g)
⊢ IsIso f

Tactic:
rw [← comp_id f, ← hom_inv_id g, ← assoc]

Result:
C : Type u
inst✝² : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsIso g
inst✝ : IsIso (f ≫ g)
⊢ IsIso ((f ≫ g) ≫ inv g)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsIso g
inst✝ : IsIso (f ≫ g)
⊢ IsIso ((f ≫ g) ≫ inv g)

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Basic.lean
theorem mem_incidence_iff_neighbor {v w : V} :
    s(v, w) ∈ G.incidenceSet v ↔ w ∈ G.neighborSet v

Proof state:
V : Type u
G : SimpleGraph V
v w : V
⊢ s(v, w) ∈ G.incidenceSet v ↔ w ∈ G.neighborSet v

Tactic:
simp only [mem_incidenceSet, mem_neighborSet]

Result:
no goals
-- Mathlib/LinearAlgebra/Reflection.lean
/-- This rather technical-looking lemma exists because it is exactly what is needed to establish a
uniqueness result for root data. See the doc string of `Module.Dual.eq_of_preReflection_mapsTo` for
further remarks. -/
lemma Dual.eq_of_preReflection_mapsTo' [CharZero R] [NoZeroSMulDivisors R M]
    {x : M} {Φ : Set M} (hΦ₁ : Φ.Finite) (hx : x ∈ span R Φ) {f g : Dual R M}
    (hf₁ : f x = 2) (hf₂ : MapsTo (preReflection x f) Φ Φ)
    (hg₁ : g x = 2) (hg₂ : MapsTo (preReflection x g) Φ Φ) :
    (span R Φ).subtype.dualMap f = (span R Φ).subtype.dualMap g

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CharZero R
inst✝ : NoZeroSMulDivisors R M
x : M
Φ : Set M
hΦ₁ : Finite ↑Φ
hx : x ∈ span R Φ
f g : Dual R M
hf₁ : f x = 2
hf₂ : MapsTo (⇑(preReflection x f)) Φ Φ
hg₁ : g x = 2
hg₂ : MapsTo (⇑(preReflection x g)) Φ Φ
Φ' : Set ↥(span R Φ) := range (inclusion ⋯)
hΦ'₁ : Φ'.Finite
⊢ (span R Φ).subtype.dualMap f = (span R Φ).subtype.dualMap g

Tactic:
have hΦ'₂ : span R Φ' = ⊤ := by
  simp only [Φ']
  rw [range_inclusion]
  simp

Result:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CharZero R
inst✝ : NoZeroSMulDivisors R M
x : M
Φ : Set M
hΦ₁ : Finite ↑Φ
hx : x ∈ span R Φ
f g : Dual R M
hf₁ : f x = 2
hf₂ : MapsTo (⇑(preReflection x f)) Φ Φ
hg₁ : g x = 2
hg₂ : MapsTo (⇑(preReflection x g)) Φ Φ
Φ' : Set ↥(span R Φ) := range (inclusion ⋯)
hΦ'₁ : Φ'.Finite
hΦ'₂ : span R Φ' = ⊤
⊢ (span R Φ).subtype.dualMap f = (span R Φ).subtype.dualMap g

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CharZero R
inst✝ : NoZeroSMulDivisors R M
x : M
Φ : Set M
hΦ₁ : Finite ↑Φ
hx : x ∈ span R Φ
f g : Dual R M
hf₁ : f x = 2
hf₂ : MapsTo (⇑(preReflection x f)) Φ Φ
hg₁ : g x = 2
hg₂ : MapsTo (⇑(preReflection x g)) Φ Φ
Φ' : Set ↥(span R Φ) := range (inclusion ⋯)
hΦ'₁ : Φ'.Finite
hΦ'₂ : span R Φ' = ⊤
⊢ (span R Φ).subtype.dualMap f = (span R Φ).subtype.dualMap g

Tactic:
let x' : span R Φ := ⟨x, hx⟩

Result:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CharZero R
inst✝ : NoZeroSMulDivisors R M
x : M
Φ : Set M
hΦ₁ : Finite ↑Φ
hx : x ∈ span R Φ
f g : Dual R M
hf₁ : f x = 2
hf₂ : MapsTo (⇑(preReflection x f)) Φ Φ
hg₁ : g x = 2
hg₂ : MapsTo (⇑(preReflection x g)) Φ Φ
Φ' : Set ↥(span R Φ) := range (inclusion ⋯)
hΦ'₁ : Φ'.Finite
hΦ'₂ : span R Φ' = ⊤
x' : ↥(span R Φ) := ⟨x, hx⟩
⊢ (span R Φ).subtype.dualMap f = (span R Φ).subtype.dualMap g
-- Mathlib/Algebra/Algebra/Subalgebra/MulOpposite.lean
theorem unop_adjoin (s : Set Aᵐᵒᵖ) :
    (Algebra.adjoin R s).unop = Algebra.adjoin R (MulOpposite.op ⁻¹' s)

Proof state:
case a
R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set Aᵐᵒᵖ
⊢ (Algebra.adjoin R s).unop.toSubsemiring = (Algebra.adjoin R (MulOpposite.op ⁻¹' s)).toSubsemiring

Tactic:
simp_rw [Algebra.adjoin, unop_toSubsemiring, Subsemiring.unop_closure, Set.preimage_union]

Result:
case a
R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set Aᵐᵒᵖ
⊢ Subsemiring.closure (MulOpposite.op ⁻¹' Set.range ⇑(algebraMap R Aᵐᵒᵖ) ∪ MulOpposite.op ⁻¹' s) =
    Subsemiring.closure (Set.range ⇑(algebraMap R A) ∪ MulOpposite.op ⁻¹' s)

Proof state:
case a
R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set Aᵐᵒᵖ
⊢ Subsemiring.closure (MulOpposite.op ⁻¹' Set.range ⇑(algebraMap R Aᵐᵒᵖ) ∪ MulOpposite.op ⁻¹' s) =
    Subsemiring.closure (Set.range ⇑(algebraMap R A) ∪ MulOpposite.op ⁻¹' s)

Tactic:
congr with x

Result:
case a.e_s.e_a.h
R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set Aᵐᵒᵖ
x : A
⊢ x ∈ MulOpposite.op ⁻¹' Set.range ⇑(algebraMap R Aᵐᵒᵖ) ↔ x ∈ Set.range ⇑(algebraMap R A)

Proof state:
R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set Aᵐᵒᵖ
⊢ (Algebra.adjoin R s).unop = Algebra.adjoin R (MulOpposite.op ⁻¹' s)

Tactic:
apply toSubsemiring_injective

Result:
case a
R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set Aᵐᵒᵖ
⊢ (Algebra.adjoin R s).unop.toSubsemiring = (Algebra.adjoin R (MulOpposite.op ⁻¹' s)).toSubsemiring

Proof state:
case a.e_s.e_a.h
R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set Aᵐᵒᵖ
x : A
⊢ x ∈ MulOpposite.op ⁻¹' Set.range ⇑(algebraMap R Aᵐᵒᵖ) ↔ x ∈ Set.range ⇑(algebraMap R A)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/LinearCombo.lean
theorem ext {a b : LinearCombo} (w₁ : a.const = b.const) (w₂ : a.coeffs = b.coeffs) :
    a = b

Proof state:
case mk.mk
const✝ : Int
coeffs✝ : Coeffs
⊢ { const := const✝, coeffs := coeffs✝ } =
    { const := { const := const✝, coeffs := coeffs✝ }.const, coeffs := { const := const✝, coeffs := coeffs✝ }.coeffs }

Tactic:
congr

Result:
no goals

Proof state:
case mk.mk
const✝¹ : Int
coeffs✝¹ : Coeffs
const✝ : Int
coeffs✝ : Coeffs
w₁ : { const := const✝¹, coeffs := coeffs✝¹ }.const = { const := const✝, coeffs := coeffs✝ }.const
w₂ : { const := const✝¹, coeffs := coeffs✝¹ }.coeffs = { const := const✝, coeffs := coeffs✝ }.coeffs
⊢ { const := const✝¹, coeffs := coeffs✝¹ } = { const := const✝, coeffs := coeffs✝ }

Tactic:
subst w₁

Result:
case mk.mk
const✝ : Int
coeffs✝¹ coeffs✝ : Coeffs
w₂ :
  { const := const✝, coeffs := coeffs✝¹ }.coeffs =
    { const := { const := const✝, coeffs := coeffs✝¹ }.const, coeffs := coeffs✝ }.coeffs
⊢ { const := const✝, coeffs := coeffs✝¹ } =
    { const := { const := const✝, coeffs := coeffs✝¹ }.const, coeffs := coeffs✝ }

Proof state:
case mk
b : LinearCombo
const✝ : Int
coeffs✝ : Coeffs
w₁ : { const := const✝, coeffs := coeffs✝ }.const = b.const
w₂ : { const := const✝, coeffs := coeffs✝ }.coeffs = b.coeffs
⊢ { const := const✝, coeffs := coeffs✝ } = b

Tactic:
cases b

Result:
case mk.mk
const✝¹ : Int
coeffs✝¹ : Coeffs
const✝ : Int
coeffs✝ : Coeffs
w₁ : { const := const✝¹, coeffs := coeffs✝¹ }.const = { const := const✝, coeffs := coeffs✝ }.const
w₂ : { const := const✝¹, coeffs := coeffs✝¹ }.coeffs = { const := const✝, coeffs := coeffs✝ }.coeffs
⊢ { const := const✝¹, coeffs := coeffs✝¹ } = { const := const✝, coeffs := coeffs✝ }

Proof state:
a b : LinearCombo
w₁ : a.const = b.const
w₂ : a.coeffs = b.coeffs
⊢ a = b

Tactic:
cases a

Result:
case mk
b : LinearCombo
const✝ : Int
coeffs✝ : Coeffs
w₁ : { const := const✝, coeffs := coeffs✝ }.const = b.const
w₂ : { const := const✝, coeffs := coeffs✝ }.coeffs = b.coeffs
⊢ { const := const✝, coeffs := coeffs✝ } = b

Proof state:
case mk.mk
const✝ : Int
coeffs✝¹ coeffs✝ : Coeffs
w₂ :
  { const := const✝, coeffs := coeffs✝¹ }.coeffs =
    { const := { const := const✝, coeffs := coeffs✝¹ }.const, coeffs := coeffs✝ }.coeffs
⊢ { const := const✝, coeffs := coeffs✝¹ } =
    { const := { const := const✝, coeffs := coeffs✝¹ }.const, coeffs := coeffs✝ }

Tactic:
subst w₂

Result:
case mk.mk
const✝ : Int
coeffs✝ : Coeffs
⊢ { const := const✝, coeffs := coeffs✝ } =
    { const := { const := const✝, coeffs := coeffs✝ }.const, coeffs := { const := const✝, coeffs := coeffs✝ }.coeffs }
-- Mathlib/RingTheory/Coprime/Basic.lean
theorem IsRelPrime.of_add_mul_left_right (h : IsRelPrime x (y + x * z)) : IsRelPrime x y

Proof state:
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsRelPrime (y + x * z) x
⊢ IsRelPrime y x

Tactic:
exact h.of_add_mul_left_left

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsRelPrime x (y + x * z)
⊢ IsRelPrime x y

Tactic:
rw [isRelPrime_comm] at h ⊢

Result:
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsRelPrime (y + x * z) x
⊢ IsRelPrime y x
-- Mathlib/Analysis/Normed/Group/Ultra.lean
/-- All triangles are isosceles in an ultrametric normed group. -/
@[to_additive "All triangles are isosceles in an ultrametric normed additive group."]
lemma nnnorm_div_eq_max_of_nnnorm_div_ne_nnnorm_div (x y z : S) (h : ‖x / y‖₊ ≠ ‖y / z‖₊) :
    ‖x / z‖₊ = max ‖x / y‖₊ ‖y / z‖₊

Proof state:
S : Type u_1
inst✝¹ : SeminormedGroup S
inst✝ : IsUltrametricDist S
x y z : S
h : ‖x / y‖₊ ≠ ‖y / z‖₊
⊢ ‖x / z‖₊ = ‖x / y‖₊ ⊔ ‖y / z‖₊

Tactic:
simpa only [← NNReal.coe_inj, NNReal.coe_max] using
  norm_div_eq_max_of_norm_div_ne_norm_div _ _ _ (NNReal.coe_injective.ne h)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem exists_mem_push {p : α → Prop} {a : α} {xs : Array α} :
    (∃ x, ∃ _ : x ∈ xs.push a, p x) ↔ p a ∨ ∃ x, ∃ _ : x ∈ xs, p x

Proof state:
case mpr
α : Type u_1
p : α → Prop
a : α
xs : Array α
⊢ (p a ∨ ∃ x, x ∈ xs ∧ p x) → ∃ x, (x ∈ xs ∨ x = a) ∧ p x

Tactic:
rintro (h | ⟨x, h, h'⟩)

Result:
case mpr.inl
α : Type u_1
p : α → Prop
a : α
xs : Array α
h : p a
⊢ ∃ x, (x ∈ xs ∨ x = a) ∧ p x

case mpr.inr.intro.intro
α : Type u_1
p : α → Prop
a : α
xs : Array α
x : α
h : x ∈ xs
h' : p x
⊢ ∃ x, (x ∈ xs ∨ x = a) ∧ p x

Proof state:
α : Type u_1
p : α → Prop
a : α
xs : Array α
h : p a
⊢ a ∈ xs ∨ a = a

Tactic:
simp

Result:
no goals

Proof state:
case mp.intro.intro.inr
α : Type u_1
p : α → Prop
xs : Array α
x : α
h' : p x
⊢ p x ∨ ∃ x, x ∈ xs ∧ p x

Tactic:
exact .inl h'

Result:
no goals

Proof state:
case mp
α : Type u_1
p : α → Prop
a : α
xs : Array α
⊢ (∃ x, (x ∈ xs ∨ x = a) ∧ p x) → p a ∨ ∃ x, x ∈ xs ∧ p x

Tactic:
rintro ⟨x, (h | rfl), h'⟩

Result:
case mp.intro.intro.inl
α : Type u_1
p : α → Prop
a : α
xs : Array α
x : α
h' : p x
h : x ∈ xs
⊢ p a ∨ ∃ x, x ∈ xs ∧ p x

case mp.intro.intro.inr
α : Type u_1
p : α → Prop
xs : Array α
x : α
h' : p x
⊢ p x ∨ ∃ x, x ∈ xs ∧ p x

Proof state:
case mp.intro.intro.inl
α : Type u_1
p : α → Prop
a : α
xs : Array α
x : α
h' : p x
h : x ∈ xs
⊢ p a ∨ ∃ x, x ∈ xs ∧ p x

Tactic:
exact .inr ⟨x, h, h'⟩

Result:
no goals

Proof state:
case mpr.inl
α : Type u_1
p : α → Prop
a : α
xs : Array α
h : p a
⊢ ∃ x, (x ∈ xs ∨ x = a) ∧ p x

Tactic:
exact ⟨a, by simp, h⟩

Result:
no goals

Proof state:
case mpr.inr.intro.intro
α : Type u_1
p : α → Prop
a : α
xs : Array α
x : α
h : x ∈ xs
h' : p x
⊢ ∃ x, (x ∈ xs ∨ x = a) ∧ p x

Tactic:
exact ⟨x, .inl h, h'⟩

Result:
no goals

Proof state:
α : Type u_1
p : α → Prop
a : α
xs : Array α
⊢ (∃ x x_1, p x) ↔ p a ∨ ∃ x x_1, p x

Tactic:
simp only [mem_push, exists_prop]

Result:
α : Type u_1
p : α → Prop
a : α
xs : Array α
⊢ (∃ x, (x ∈ xs ∨ x = a) ∧ p x) ↔ p a ∨ ∃ x, x ∈ xs ∧ p x

Proof state:
α : Type u_1
p : α → Prop
a : α
xs : Array α
⊢ (∃ x, (x ∈ xs ∨ x = a) ∧ p x) ↔ p a ∨ ∃ x, x ∈ xs ∧ p x

Tactic:
constructor

Result:
case mp
α : Type u_1
p : α → Prop
a : α
xs : Array α
⊢ (∃ x, (x ∈ xs ∨ x = a) ∧ p x) → p a ∨ ∃ x, x ∈ xs ∧ p x

case mpr
α : Type u_1
p : α → Prop
a : α
xs : Array α
⊢ (p a ∨ ∃ x, x ∈ xs ∧ p x) → ∃ x, (x ∈ xs ∨ x = a) ∧ p x
-- Mathlib/RingTheory/Adjoin/FG.lean
theorem fg_trans (h1 : (adjoin R s).toSubmodule.FG) (h2 : (adjoin (adjoin R s) t).toSubmodule.FG) :
    (adjoin R (s ∪ t)).toSubmodule.FG

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
x : A
hx : x ∈ p
y : A
hy : y ∈ q
⊢ x ∈ Subalgebra.toSubmodule (adjoin R s)

Tactic:
rw [← hp']

Result:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
x : A
hx : x ∈ p
y : A
hy : y ∈ q
⊢ x ∈ span R p

Proof state:
case intro.intro
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
⊢ (Subalgebra.toSubmodule (adjoin R (s ∪ t))).FG

Tactic:
rcases fg_def.1 h2 with ⟨q, hq, hq'⟩

Result:
case intro.intro.intro.intro
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
⊢ (Subalgebra.toSubmodule (adjoin R (s ∪ t))).FG
-- Mathlib/Data/List/Sublists.lean
theorem sublistsLenAux_eq (l : List α) (n) (f : List α → β) (r) :
    sublistsLenAux n l f r = (sublistsLen n l).map f ++ r

Proof state:
α : Type u
β : Type v
l : List α
n : ℕ
f : List α → β
r : List β
⊢ sublistsLenAux n l f r = sublistsLenAux n l (f ∘ id) (map f [] ++ r)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
β : Type v
l : List α
n : ℕ
f : List α → β
r : List β
⊢ sublistsLenAux n l f r = map f (sublistsLen n l) ++ r

Tactic:
rw [sublistsLen, ← sublistsLenAux_append]

Result:
α : Type u
β : Type v
l : List α
n : ℕ
f : List α → β
r : List β
⊢ sublistsLenAux n l f r = sublistsLenAux n l (f ∘ id) (map f [] ++ r)
-- Mathlib/Algebra/Polynomial/Div.lean
lemma associated_of_dvd_of_natDegree_le_of_leadingCoeff {p q : R[X]} (hpq : p ∣ q)
    (h₁ : q.natDegree ≤ p.natDegree) (h₂ : q.leadingCoeff ∣ p.leadingCoeff) :
    Associated p q :=
  have ⟨r, hr⟩ := hpq
  have ⟨u, hu⟩ := associated_of_dvd_dvd ⟨leadingCoeff r, hr ▸ leadingCoeff_mul p r⟩ h₂
  ⟨Units.map C.toMonoidHom u, eq_of_dvd_of_natDegree_le_of_leadingCoeff
    (by rwa [Units.mul_right_dvd]) (by simpa [natDegree_mul_C] using h₁) (by simpa using hu)⟩

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hpq : p ∣ q
h₁ : q.natDegree ≤ p.natDegree
h₂ : q.leadingCoeff ∣ p.leadingCoeff
r : R[X]
hr : q = p * r
u : Rˣ
hu : p.leadingCoeff * ↑u = q.leadingCoeff
⊢ (p * ↑((Units.map ↑C) u)).leadingCoeff = q.leadingCoeff

Tactic:
simpa using hu

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hpq : p ∣ q
h₁ : q.natDegree ≤ p.natDegree
h₂ : q.leadingCoeff ∣ p.leadingCoeff
r : R[X]
hr : q = p * r
u : Rˣ
hu : p.leadingCoeff * ↑u = q.leadingCoeff
⊢ p * ↑((Units.map ↑C) u) ∣ q

Tactic:
rwa [Units.mul_right_dvd]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hpq : p ∣ q
h₁ : q.natDegree ≤ p.natDegree
h₂ : q.leadingCoeff ∣ p.leadingCoeff
r : R[X]
hr : q = p * r
u : Rˣ
hu : p.leadingCoeff * ↑u = q.leadingCoeff
⊢ q.natDegree ≤ (p * ↑((Units.map ↑C) u)).natDegree

Tactic:
simpa [natDegree_mul_C] using h₁

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDimension.lean
theorem dimH_countable {s : Set X} (hs : s.Countable) : dimH s = 0 :=
  biUnion_of_singleton s ▸ by simp only [dimH_bUnion hs, dimH_singleton, ENNReal.iSup_zero]

Proof state:
X : Type u_2
inst✝ : EMetricSpace X
s : Set X
hs : s.Countable
⊢ dimH (⋃ x ∈ s, {x}) = 0

Tactic:
simp only [dimH_bUnion hs, dimH_singleton, ENNReal.iSup_zero]

Result:
no goals
-- Mathlib/Analysis/Convex/Combination.lean
theorem affineCombination_mem_convexHull {s : Finset ι} {v : ι → E} {w : ι → R}
    (hw₀ : ∀ i ∈ s, 0 ≤ w i) (hw₁ : s.sum w = 1) :
    s.affineCombination R v w ∈ convexHull R (range v)

Proof state:
case hws
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset ι
v : ι → E
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
⊢ 0 < ∑ i ∈ s, w i

Tactic:
simp [hw₁]

Result:
no goals

Proof state:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset ι
v : ι → E
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
⊢ (affineCombination R s v) w ∈ (convexHull R) (Set.range v)

Tactic:
rw [affineCombination_eq_centerMass hw₁]

Result:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset ι
v : ι → E
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
⊢ s.centerMass w v ∈ (convexHull R) (Set.range v)

Proof state:
case hz
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset ι
v : ι → E
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
⊢ ∀ i ∈ s, v i ∈ Set.range v

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset ι
v : ι → E
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
⊢ s.centerMass w v ∈ (convexHull R) (Set.range v)

Tactic:
apply s.centerMass_mem_convexHull hw₀

Result:
case hws
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset ι
v : ι → E
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
⊢ 0 < ∑ i ∈ s, w i

case hz
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset ι
v : ι → E
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
⊢ ∀ i ∈ s, v i ∈ Set.range v
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem eq_prod_range_div' {M : Type*} [CommGroup M] (f : ℕ → M) (n : ℕ) :
    f n = ∏ i ∈ range (n + 1), if i = 0 then f 0 else f i / f (i - 1)

Proof state:
M : Type u_6
inst✝ : CommGroup M
f : ℕ → M
n : ℕ
⊢ f n = ∏ i ∈ range (n + 1), if i = 0 then f 0 else f i / f (i - 1)

Tactic:
conv_lhs => rw [Finset.eq_prod_range_div f]

Result:
M : Type u_6
inst✝ : CommGroup M
f : ℕ → M
n : ℕ
⊢ f 0 * ∏ i ∈ range n, f (i + 1) / f i = ∏ i ∈ range (n + 1), if i = 0 then f 0 else f i / f (i - 1)

Proof state:
M : Type u_6
inst✝ : CommGroup M
f : ℕ → M
n : ℕ
⊢ f 0 * ∏ i ∈ range n, f (i + 1) / f i = ∏ i ∈ range (n + 1), if i = 0 then f 0 else f i / f (i - 1)

Tactic:
simp [Finset.prod_range_succ', mul_comm]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Hom.lean
theorem inverse'_comp {f : X →ₑ[φ] Y} {g : Y → X}
    {k₂ : Function.RightInverse φ' φ}
    {h₁ : Function.LeftInverse g f} {h₂ : Function.RightInverse g f} :
    f.comp (inverse' f g k₂ h₁ h₂) (κ := CompTriple.comp_inv k₂) = MulActionHom.id N

Proof state:
M : Type u_2
N : Type u_3
φ : M → N
X : Type u_5
inst✝¹ : SMul M X
Y : Type u_6
inst✝ : SMul N Y
φ' : N → M
f : X →ₑ[φ] Y
g : Y → X
k₂ : Function.RightInverse φ' φ
h₁ : Function.LeftInverse g ⇑f
h₂ : Function.RightInverse g ⇑f
⊢ ∀ (x : Y), (f.comp (f.inverse' g k₂ h₁ h₂)) x = (MulActionHom.id N) x

Tactic:
intro x

Result:
M : Type u_2
N : Type u_3
φ : M → N
X : Type u_5
inst✝¹ : SMul M X
Y : Type u_6
inst✝ : SMul N Y
φ' : N → M
f : X →ₑ[φ] Y
g : Y → X
k₂ : Function.RightInverse φ' φ
h₁ : Function.LeftInverse g ⇑f
h₂ : Function.RightInverse g ⇑f
x : Y
⊢ (f.comp (f.inverse' g k₂ h₁ h₂)) x = (MulActionHom.id N) x

Proof state:
M : Type u_2
N : Type u_3
φ : M → N
X : Type u_5
inst✝¹ : SMul M X
Y : Type u_6
inst✝ : SMul N Y
φ' : N → M
f : X →ₑ[φ] Y
g : Y → X
k₂ : Function.RightInverse φ' φ
h₁ : Function.LeftInverse g ⇑f
h₂ : Function.RightInverse g ⇑f
x : Y
⊢ f ((f.inverse' g k₂ h₁ h₂) x) = x

Tactic:
exact h₂ x

Result:
no goals

Proof state:
M : Type u_2
N : Type u_3
φ : M → N
X : Type u_5
inst✝¹ : SMul M X
Y : Type u_6
inst✝ : SMul N Y
φ' : N → M
f : X →ₑ[φ] Y
g : Y → X
k₂ : Function.RightInverse φ' φ
h₁ : Function.LeftInverse g ⇑f
h₂ : Function.RightInverse g ⇑f
x : Y
⊢ (f.comp (f.inverse' g k₂ h₁ h₂)) x = (MulActionHom.id N) x

Tactic:
simp only [comp_apply, inverse_apply, id_apply]

Result:
M : Type u_2
N : Type u_3
φ : M → N
X : Type u_5
inst✝¹ : SMul M X
Y : Type u_6
inst✝ : SMul N Y
φ' : N → M
f : X →ₑ[φ] Y
g : Y → X
k₂ : Function.RightInverse φ' φ
h₁ : Function.LeftInverse g ⇑f
h₂ : Function.RightInverse g ⇑f
x : Y
⊢ f ((f.inverse' g k₂ h₁ h₂) x) = x

Proof state:
M : Type u_2
N : Type u_3
φ : M → N
X : Type u_5
inst✝¹ : SMul M X
Y : Type u_6
inst✝ : SMul N Y
φ' : N → M
f : X →ₑ[φ] Y
g : Y → X
k₂ : Function.RightInverse φ' φ
h₁ : Function.LeftInverse g ⇑f
h₂ : Function.RightInverse g ⇑f
⊢ f.comp (f.inverse' g k₂ h₁ h₂) = MulActionHom.id N

Tactic:
rw [MulActionHom.ext_iff]

Result:
M : Type u_2
N : Type u_3
φ : M → N
X : Type u_5
inst✝¹ : SMul M X
Y : Type u_6
inst✝ : SMul N Y
φ' : N → M
f : X →ₑ[φ] Y
g : Y → X
k₂ : Function.RightInverse φ' φ
h₁ : Function.LeftInverse g ⇑f
h₂ : Function.RightInverse g ⇑f
⊢ ∀ (x : Y), (f.comp (f.inverse' g k₂ h₁ h₂)) x = (MulActionHom.id N) x
-- Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean
theorem degree_eq_sum_if_adj {R : Type*} [AddCommMonoidWithOne R] (i : V) :
    (G.degree i : R) = ∑ j : V, if G.Adj i j then 1 else 0

Proof state:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
R : Type u_3
inst✝ : AddCommMonoidWithOne R
i : V
⊢ ↑(#{w | G.Adj i w}.toFinset) = ∑ j : V, if G.Adj i j then 1 else 0

Tactic:
rw [sum_boole, Set.toFinset_setOf]

Result:
no goals

Proof state:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
R : Type u_3
inst✝ : AddCommMonoidWithOne R
i : V
⊢ ↑(G.degree i) = ∑ j : V, if G.Adj i j then 1 else 0

Tactic:
unfold degree neighborFinset neighborSet

Result:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
R : Type u_3
inst✝ : AddCommMonoidWithOne R
i : V
⊢ ↑(#{w | G.Adj i w}.toFinset) = ∑ j : V, if G.Adj i j then 1 else 0