harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Euclidean/Sphere/SecondInter.lean
theorem Sphere.secondInter_dist (s : Sphere P) (p : P) (v : V) :
    dist (s.secondInter p v) s.center = dist p s.center

Proof state:
case neg
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
v : V
hv : ¬v = 0
⊢ dist ((-2 * inner v (p -ᵥ s.center) / inner v v) • v +ᵥ p) s.center = dist p s.center

Tactic:
rw [dist_smul_vadd_eq_dist _ _ hv]

Result:
case neg
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
v : V
hv : ¬v = 0
⊢ -2 * inner v (p -ᵥ s.center) / inner v v = 0 ∨
    -2 * inner v (p -ᵥ s.center) / inner v v = -2 * inner v (p -ᵥ s.center) / inner v v

Proof state:
case pos
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
v : V
hv : v = 0
⊢ dist ((-2 * inner v (p -ᵥ s.center) / inner v v) • v +ᵥ p) s.center = dist p s.center

Tactic:
simp [hv]

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
v : V
⊢ dist ((-2 * inner v (p -ᵥ s.center) / inner v v) • v +ᵥ p) s.center = dist p s.center

Tactic:
by_cases hv : v = 0

Result:
case pos
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
v : V
hv : v = 0
⊢ dist ((-2 * inner v (p -ᵥ s.center) / inner v v) • v +ᵥ p) s.center = dist p s.center

case neg
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
v : V
hv : ¬v = 0
⊢ dist ((-2 * inner v (p -ᵥ s.center) / inner v v) • v +ᵥ p) s.center = dist p s.center

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
v : V
⊢ dist (s.secondInter p v) s.center = dist p s.center

Tactic:
rw [Sphere.secondInter]

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
v : V
⊢ dist ((-2 * inner v (p -ᵥ s.center) / inner v v) • v +ᵥ p) s.center = dist p s.center

Proof state:
case neg
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
v : V
hv : ¬v = 0
⊢ -2 * inner v (p -ᵥ s.center) / inner v v = 0 ∨
    -2 * inner v (p -ᵥ s.center) / inner v v = -2 * inner v (p -ᵥ s.center) / inner v v

Tactic:
exact Or.inr rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem liftOrGet_eq_or_eq {f : α → α → α} (h : ∀ a b, f a b = a ∨ f a b = b) :
    ∀ o₁ o₂, liftOrGet f o₁ o₂ = o₁ ∨ liftOrGet f o₁ o₂ = o₂
  | none, none => .inl rfl
  | some _, none => .inl rfl
  | none, some _ => .inr rfl
  | some a, some b => by have := h a b; simp [liftOrGet] at this ⊢; exact this

Proof state:
α : Type u_1
f : α → α → α
h : ∀ (a b : α), f a b = a ∨ f a b = b
a b : α
this : f a b = a ∨ f a b = b
⊢ f a b = a ∨ f a b = b

Tactic:
exact this

Result:
no goals

Proof state:
α : Type u_1
f : α → α → α
h : ∀ (a b : α), f a b = a ∨ f a b = b
a b : α
⊢ liftOrGet f (some a) (some b) = some a ∨ liftOrGet f (some a) (some b) = some b

Tactic:
have := h a b

Result:
α : Type u_1
f : α → α → α
h : ∀ (a b : α), f a b = a ∨ f a b = b
a b : α
this : f a b = a ∨ f a b = b
⊢ liftOrGet f (some a) (some b) = some a ∨ liftOrGet f (some a) (some b) = some b

Proof state:
α : Type u_1
f : α → α → α
h : ∀ (a b : α), f a b = a ∨ f a b = b
a b : α
this : f a b = a ∨ f a b = b
⊢ liftOrGet f (some a) (some b) = some a ∨ liftOrGet f (some a) (some b) = some b

Tactic:
simp [liftOrGet] at this ⊢

Result:
α : Type u_1
f : α → α → α
h : ∀ (a b : α), f a b = a ∨ f a b = b
a b : α
this : f a b = a ∨ f a b = b
⊢ f a b = a ∨ f a b = b
-- Mathlib/Algebra/MvPolynomial/CommRing.lean
theorem vars_sub_of_disjoint [DecidableEq σ] (hpq : Disjoint p.vars q.vars) :
    (p - q).vars = p.vars ∪ q.vars

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommRing R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
hpq : Disjoint p.vars q.vars
⊢ (p - q).vars = p.vars ∪ q.vars

Tactic:
rw [← vars_neg q] at hpq

Result:
R : Type u
σ : Type u_1
inst✝¹ : CommRing R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
hpq : Disjoint p.vars (-q).vars
⊢ (p - q).vars = p.vars ∪ q.vars

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommRing R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
hpq : Disjoint p.vars (-q).vars
⊢ (p - q).vars = p.vars ∪ q.vars

Tactic:
convert vars_add_of_disjoint hpq using 2 <;> simp [sub_eq_add_neg]

Result:
no goals
-- Mathlib/SetTheory/Surreal/Multiplication.lean
lemma ih4 (ih' : ∀ a, ArgsRel a (Args.P24 x₁ x₂ y) → P124 a) : IH4 x₁ x₂ y

Proof state:
case refine_2
x₁ x₂ y : PGame
ih' : ∀ (a : Args), ArgsRel a (Args.P24 x₁ x₂ y) → P124 a
z w : PGame
h : w.IsOption y
h' : z.IsOption x₂
⊢ P2 x₁ z w

Tactic:
apply (ih' (Args.P24 _ _ _) <| (TransGen.single _).tail <|
  (cutExpand_add_left {x₁}).2 <| cutExpand_pair_right h).1

Result:
x₁ x₂ y : PGame
ih' : ∀ (a : Args), ArgsRel a (Args.P24 x₁ x₂ y) → P124 a
z w : PGame
h : w.IsOption y
h' : z.IsOption x₂
⊢ CutExpand IsOption (Args.P24 x₁ z w).toMultiset ({x₁} + {x₂, w})

Proof state:
x₁ x₂ y : PGame
ih' : ∀ (a : Args), ArgsRel a (Args.P24 x₁ x₂ y) → P124 a
z w : PGame
h : w.IsOption y
h' : z.IsOption x₁
⊢ CutExpand IsOption (Args.P24 z x₂ w).toMultiset ({x₁} + {x₂, w})

Tactic:
try exact (cutExpand_add_right {w}).2 <| cutExpand_pair_left h'

Result:
no goals

Proof state:
x₁ x₂ y : PGame
ih' : ∀ (a : Args), ArgsRel a (Args.P24 x₁ x₂ y) → P124 a
⊢ IH4 x₁ x₂ y

Tactic:
refine fun z w h ↦ ⟨?_, ?_⟩

Result:
case refine_1
x₁ x₂ y : PGame
ih' : ∀ (a : Args), ArgsRel a (Args.P24 x₁ x₂ y) → P124 a
z w : PGame
h : w.IsOption y
⊢ z.IsOption x₁ → P2 z x₂ w

case refine_2
x₁ x₂ y : PGame
ih' : ∀ (a : Args), ArgsRel a (Args.P24 x₁ x₂ y) → P124 a
z w : PGame
h : w.IsOption y
⊢ z.IsOption x₂ → P2 x₁ z w

Proof state:
x₁ x₂ y : PGame
ih' : ∀ (a : Args), ArgsRel a (Args.P24 x₁ x₂ y) → P124 a
z w : PGame
h : w.IsOption y
h' : z.IsOption x₂
⊢ CutExpand IsOption (Args.P24 x₁ z w).toMultiset ({x₁} + {x₂, w})

Tactic:
try exact (cutExpand_add_right {w}).2 <| cutExpand_pair_right h'

Result:
no goals

Proof state:
case refine_1
x₁ x₂ y : PGame
ih' : ∀ (a : Args), ArgsRel a (Args.P24 x₁ x₂ y) → P124 a
z w : PGame
h : w.IsOption y
⊢ z.IsOption x₁ → P2 z x₂ w

case refine_2
x₁ x₂ y : PGame
ih' : ∀ (a : Args), ArgsRel a (Args.P24 x₁ x₂ y) → P124 a
z w : PGame
h : w.IsOption y
⊢ z.IsOption x₂ → P2 x₁ z w

Tactic:
all_goals
  intro h'
  apply (ih' (Args.P24 _ _ _) <| (TransGen.single _).tail <|
    (cutExpand_add_left {x₁}).2 <| cutExpand_pair_right h).1
  try exact (cutExpand_add_right {w}).2 <| cutExpand_pair_left h'
  try exact (cutExpand_add_right {w}).2 <| cutExpand_pair_right h'

Result:
no goals

Proof state:
x₁ x₂ y : PGame
ih' : ∀ (a : Args), ArgsRel a (Args.P24 x₁ x₂ y) → P124 a
z w : PGame
h : w.IsOption y
h' : z.IsOption x₁
⊢ CutExpand IsOption (Args.P24 z x₂ w).toMultiset ({x₁} + {x₂, w})

Tactic:
exact (cutExpand_add_right {w}).2 <| cutExpand_pair_left h'

Result:
no goals

Proof state:
case refine_2
x₁ x₂ y : PGame
ih' : ∀ (a : Args), ArgsRel a (Args.P24 x₁ x₂ y) → P124 a
z w : PGame
h : w.IsOption y
⊢ z.IsOption x₂ → P2 x₁ z w

Tactic:
intro h'

Result:
case refine_2
x₁ x₂ y : PGame
ih' : ∀ (a : Args), ArgsRel a (Args.P24 x₁ x₂ y) → P124 a
z w : PGame
h : w.IsOption y
h' : z.IsOption x₂
⊢ P2 x₁ z w

Proof state:
x₁ x₂ y : PGame
ih' : ∀ (a : Args), ArgsRel a (Args.P24 x₁ x₂ y) → P124 a
z w : PGame
h : w.IsOption y
h' : z.IsOption x₂
⊢ CutExpand IsOption (Args.P24 x₁ z w).toMultiset ({x₁} + {x₂, w})

Tactic:
exact (cutExpand_add_right {w}).2 <| cutExpand_pair_right h'

Result:
no goals
-- Mathlib/Data/Fin/Parity.lean
lemma even_of_odd {n : ℕ} (hn : Odd n) (k : Fin n) : Even k

Proof state:
n : ℕ
hn : Odd n
k : Fin n
⊢ Even k

Tactic:
have : NeZero n := ⟨k.pos.ne'⟩

Result:
n : ℕ
hn : Odd n
k : Fin n
this : NeZero n
⊢ Even k

Proof state:
n : ℕ
hn : Odd n
k : Fin n
this : NeZero n
⊢ Even k

Tactic:
rcases k.val.even_or_odd with hk | hk

Result:
case inl
n : ℕ
hn : Odd n
k : Fin n
this : NeZero n
hk : Even ↑k
⊢ Even k

case inr
n : ℕ
hn : Odd n
k : Fin n
this : NeZero n
hk : Odd ↑k
⊢ Even k

Proof state:
case inl
n : ℕ
hn : Odd n
k : Fin n
this : NeZero n
hk : Even ↑k
⊢ Even k

Tactic:
exact even_of_val hk

Result:
no goals

Proof state:
case inr
n : ℕ
hn : Odd n
k : Fin n
this : NeZero n
hk : Odd ↑k
⊢ Even k

Tactic:
simpa using (hk.add_odd hn).natCast (α := Fin n)

Result:
no goals
-- Mathlib/Analysis/Fourier/FiniteAbelian/Orthogonality.lean
lemma expect_eq_ite (ψ : AddChar G R) : 𝔼 a, ψ a = if ψ = 0 then 1 else 0

Proof state:
G : Type u_1
R : Type u_3
inst✝⁴ : AddGroup G
inst✝³ : Fintype G
inst✝² : Semifield R
inst✝¹ : IsDomain R
inst✝ : CharZero R
ψ : AddChar G R
⊢ 𝔼 a : G, ψ a = if ψ = 0 then 1 else 0

Tactic:
simp [Fintype.expect_eq_sum_div_card, sum_eq_ite, ite_div]

Result:
no goals
-- Mathlib/Data/Finset/Union.lean
lemma disjoint_biUnion_right (s : Finset β) (t : Finset α) (f : α → Finset β) :
    Disjoint s (t.biUnion f) ↔ ∀ i ∈ t, Disjoint s (f i)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset β
t : Finset α
f : α → Finset β
⊢ Disjoint s (t.biUnion f) ↔ ∀ i ∈ t, Disjoint s (f i)

Tactic:
simpa only [_root_.disjoint_comm] using disjoint_biUnion_left t f s

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem xor_assoc (x y z : Nat) : (x ^^^ y) ^^^ z = x ^^^ (y ^^^ z)

Proof state:
case pred
x y z : Nat
⊢ ∀ (i : Nat), (x ^^^ y ^^^ z).testBit i = (x ^^^ (y ^^^ z)).testBit i

Tactic:
simp

Result:
no goals

Proof state:
x y z : Nat
⊢ x ^^^ y ^^^ z = x ^^^ (y ^^^ z)

Tactic:
apply Nat.eq_of_testBit_eq

Result:
case pred
x y z : Nat
⊢ ∀ (i : Nat), (x ^^^ y ^^^ z).testBit i = (x ^^^ (y ^^^ z)).testBit i
-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem Ideal.mem_normalizedFactors_iff {p I : Ideal A} (hI : I ≠ ⊥) :
    p ∈ normalizedFactors I ↔ p.IsPrime ∧ I ≤ p

Proof state:
case pos
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
p I : Ideal A
hI : I ≠ ⊥
hp : p = 0
⊢ p ∈ normalizedFactors I ↔ p.IsPrime ∧ p ∣ I

Tactic:
rw [← zero_eq_bot] at hI

Result:
case pos
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
p I : Ideal A
hI : I ≠ 0
hp : p = 0
⊢ p ∈ normalizedFactors I ↔ p.IsPrime ∧ p ∣ I

Proof state:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
p I : Ideal A
hI : I ≠ ⊥
⊢ p ∈ normalizedFactors I ↔ p.IsPrime ∧ I ≤ p

Tactic:
rw [← Ideal.dvd_iff_le]

Result:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
p I : Ideal A
hI : I ≠ ⊥
⊢ p ∈ normalizedFactors I ↔ p.IsPrime ∧ p ∣ I

Proof state:
case neg
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
p I : Ideal A
hI : I ≠ ⊥
hp : ¬p = 0
⊢ p ∈ normalizedFactors I ↔ p.IsPrime ∧ p ∣ I

Tactic:
rwa [mem_normalizedFactors_iff hI, prime_iff_isPrime]

Result:
no goals

Proof state:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
p I : Ideal A
hI : I ≠ ⊥
⊢ p ∈ normalizedFactors I ↔ p.IsPrime ∧ p ∣ I

Tactic:
by_cases hp : p = 0

Result:
case pos
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
p I : Ideal A
hI : I ≠ ⊥
hp : p = 0
⊢ p ∈ normalizedFactors I ↔ p.IsPrime ∧ p ∣ I

case neg
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
p I : Ideal A
hI : I ≠ ⊥
hp : ¬p = 0
⊢ p ∈ normalizedFactors I ↔ p.IsPrime ∧ p ∣ I

Proof state:
case pos
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
p I : Ideal A
hI : I ≠ 0
hp : p = 0
⊢ p ∈ normalizedFactors I ↔ p.IsPrime ∧ p ∣ I

Tactic:
simp only [hp, zero_not_mem_normalizedFactors, zero_dvd_iff, hI, false_iff, not_and,
  not_false_eq_true, implies_true]

Result:
no goals
-- Mathlib/Data/Finsupp/Basic.lean
theorem prod_filter_index [CommMonoid N] (g : α → M → N) :
    (f.filter p).prod g = ∏ x ∈ (f.filter p).support, g x (f x)

Proof state:
α : Type u_1
M : Type u_5
N : Type u_7
inst✝² : Zero M
p : α → Prop
inst✝¹ : DecidablePred p
f : α →₀ M
inst✝ : CommMonoid N
g : α → M → N
⊢ (filter p f).prod g = ∏ x ∈ (filter p f).support, g x (f x)

Tactic:
refine Finset.prod_congr rfl fun x hx => ?_

Result:
α : Type u_1
M : Type u_5
N : Type u_7
inst✝² : Zero M
p : α → Prop
inst✝¹ : DecidablePred p
f : α →₀ M
inst✝ : CommMonoid N
g : α → M → N
x : α
hx : x ∈ (filter p f).support
⊢ g x ((filter p f) x) = g x (f x)

Proof state:
α : Type u_1
M : Type u_5
N : Type u_7
inst✝² : Zero M
p : α → Prop
inst✝¹ : DecidablePred p
f : α →₀ M
inst✝ : CommMonoid N
g : α → M → N
x : α
hx : x ∈ (filter p f).support
⊢ g x ((filter p f) x) = g x (f x)

Tactic:
rw [support_filter, Finset.mem_filter] at hx

Result:
α : Type u_1
M : Type u_5
N : Type u_7
inst✝² : Zero M
p : α → Prop
inst✝¹ : DecidablePred p
f : α →₀ M
inst✝ : CommMonoid N
g : α → M → N
x : α
hx : x ∈ f.support ∧ p x
⊢ g x ((filter p f) x) = g x (f x)

Proof state:
α : Type u_1
M : Type u_5
N : Type u_7
inst✝² : Zero M
p : α → Prop
inst✝¹ : DecidablePred p
f : α →₀ M
inst✝ : CommMonoid N
g : α → M → N
⊢ (filter p f).prod g = ∏ x ∈ (filter p f).support, g x (f x)

Tactic:
classical
  refine Finset.prod_congr rfl fun x hx => ?_
  rw [support_filter, Finset.mem_filter] at hx
  rw [filter_apply_pos _ _ hx.2]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
N : Type u_7
inst✝² : Zero M
p : α → Prop
inst✝¹ : DecidablePred p
f : α →₀ M
inst✝ : CommMonoid N
g : α → M → N
x : α
hx : x ∈ f.support ∧ p x
⊢ g x ((filter p f) x) = g x (f x)

Tactic:
rw [filter_apply_pos _ _ hx.2]

Result:
no goals
-- Mathlib/RingTheory/Finiteness/Basic.lean
theorem FG.map {N : Submodule R M} (hs : N.FG) : (N.map f).FG :=
  let ⟨t, ht⟩ := fg_def.1 hs
  fg_def.2 ⟨f '' t, ht.1.image _, by rw [span_image, ht.2]⟩

Proof state:
R : Type u_1
M : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_3
P : Type u_4
inst✝³ : Semiring S
inst✝² : AddCommMonoid P
inst✝¹ : Module S P
σ : R →+* S
inst✝ : RingHomSurjective σ
f : M →ₛₗ[σ] P
N : Submodule R M
hs : N.FG
t : Set M
ht : t.Finite ∧ span R t = N
⊢ span S (⇑f '' t) = Submodule.map f N

Tactic:
rw [span_image, ht.2]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem map_U (f : R →+* R') (n : ℤ) : map f (U R n) = U R' n

Proof state:
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
n : ℤ
⊢ map f (U R n) = U R' n

Tactic:
induction n using Polynomial.Chebyshev.induct with
| zero => simp
| one => simp
| add_two n ih1 ih2 =>
  simp_rw [U_add_two, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X, ih1,
    ih2]
| neg_add_one n ih1 ih2 =>
  simp_rw [U_sub_one, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X, ih1,
    ih2]

Result:
no goals

Proof state:
case one
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
⊢ map f (U R 1) = U R' 1

Tactic:
simp

Result:
no goals

Proof state:
case zero
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
⊢ map f (U R 0) = U R' 0

Tactic:
simp

Result:
no goals

Proof state:
case add_two
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
n : ℕ
ih1 : map f (U R (↑n + 1)) = U R' (↑n + 1)
ih2 : map f (U R ↑n) = U R' ↑n
⊢ map f (U R (↑n + 2)) = U R' (↑n + 2)

Tactic:
simp_rw [U_add_two, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X, ih1,
  ih2]

Result:
no goals

Proof state:
case neg_add_one
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
n : ℕ
ih1 : map f (U R (-↑n)) = U R' (-↑n)
ih2 : map f (U R (-↑n + 1)) = U R' (-↑n + 1)
⊢ map f (U R (-↑n - 1)) = U R' (-↑n - 1)

Tactic:
simp_rw [U_sub_one, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X, ih1,
  ih2]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Modify.lean
theorem getElem?_modify (f : α → α) :
    ∀ n (l : List α) m, (modify f n l)[m]? = (fun a => if n = m then f a else a) <$> l[m]?
  | n, l, 0 => by cases l <;> cases n <;> simp
  | n, [], _+1 => by cases n <;> rfl
  | 0, _ :: l, m+1 => by cases h : l[m]? <;> simp [h, modify, m.succ_ne_zero.symm]
  | n+1, a :: l, m+1 => by
    simp only [modify_succ_cons, getElem?_cons_succ, Nat.reduceEqDiff, Option.map_eq_map]
    refine (getElem?_modify f n l m).trans ?_
    cases h' : l[m]? <;> by_cases h : n = m <;>
      simp [h, if_pos, if_neg, Option.map, mt Nat.succ.inj, not_false_iff, h']

Proof state:
α : Type u_1
f : α → α
head✝ : α
l : List α
m : Nat
⊢ (modify f 0 (head✝ :: l))[m + 1]? = (fun a => if 0 = m + 1 then f a else a) <$> (head✝ :: l)[m + 1]?

Tactic:
cases h : l[m]? <;> simp [h, modify, m.succ_ne_zero.symm]

Result:
no goals

Proof state:
α : Type u_1
f : α → α
n : Nat
a : α
l : List α
m : Nat
⊢ (modify f n l)[m]? = Option.map (fun a => if n + 1 = m + 1 then f a else a) l[m]?

Tactic:
refine (getElem?_modify f n l m).trans ?_

Result:
α : Type u_1
f : α → α
n : Nat
a : α
l : List α
m : Nat
⊢ (fun a => if n = m then f a else a) <$> l[m]? = Option.map (fun a => if n + 1 = m + 1 then f a else a) l[m]?

Proof state:
α : Type u_1
f : α → α
n : Nat
l : List α
⊢ (modify f n l)[0]? = (fun a => if n = 0 then f a else a) <$> l[0]?

Tactic:
cases l <;> cases n <;> simp

Result:
no goals

Proof state:
α : Type u_1
f : α → α
n : Nat
a : α
l : List α
m : Nat
⊢ (fun a => if n = m then f a else a) <$> l[m]? = Option.map (fun a => if n + 1 = m + 1 then f a else a) l[m]?

Tactic:
cases h' : l[m]? <;> by_cases h : n = m <;>
  simp [h, if_pos, if_neg, Option.map, mt Nat.succ.inj, not_false_iff, h']

Result:
no goals

Proof state:
α : Type u_1
f : α → α
n : Nat
a : α
l : List α
m : Nat
⊢ (modify f (n + 1) (a :: l))[m + 1]? = (fun a => if n + 1 = m + 1 then f a else a) <$> (a :: l)[m + 1]?

Tactic:
simp only [modify_succ_cons, getElem?_cons_succ, Nat.reduceEqDiff, Option.map_eq_map]

Result:
α : Type u_1
f : α → α
n : Nat
a : α
l : List α
m : Nat
⊢ (modify f n l)[m]? = Option.map (fun a => if n + 1 = m + 1 then f a else a) l[m]?

Proof state:
α : Type u_1
f : α → α
n n✝ : Nat
⊢ (modify f n [])[n✝ + 1]? = (fun a => if n = n✝ + 1 then f a else a) <$> [][n✝ + 1]?

Tactic:
cases n <;> rfl

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem UniformCauchySeqOnFilter.mono_left {p'' : Filter ι} (hf : UniformCauchySeqOnFilter F p p')
    (hp : p'' ≤ p) : UniformCauchySeqOnFilter F p'' p'

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
p : Filter ι
p' : Filter α
p'' : Filter ι
hf : UniformCauchySeqOnFilter F p p'
hp : p'' ≤ p
u : Set (β × β)
hu : u ∈ 𝓤 β
this : ∀ᶠ (x : (ι × ι) × α) in (p'' ×ˢ p'') ×ˢ p', (F x.1.1 x.2, F x.1.2 x.2) ∈ u
⊢ ∀ᶠ (m : (ι × ι) × α) in (p'' ×ˢ p'') ×ˢ p', (F m.1.1 m.2, F m.1.2 m.2) ∈ u

Tactic:
exact this.mono (by simp)

Result:
no goals

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
p : Filter ι
p' : Filter α
p'' : Filter ι
hf : UniformCauchySeqOnFilter F p p'
hp : p'' ≤ p
⊢ UniformCauchySeqOnFilter F p'' p'

Tactic:
intro u hu

Result:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
p : Filter ι
p' : Filter α
p'' : Filter ι
hf : UniformCauchySeqOnFilter F p p'
hp : p'' ≤ p
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ ∀ᶠ (m : (ι × ι) × α) in (p'' ×ˢ p'') ×ˢ p', (F m.1.1 m.2, F m.1.2 m.2) ∈ u

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
p : Filter ι
p' : Filter α
p'' : Filter ι
hf : UniformCauchySeqOnFilter F p p'
hp : p'' ≤ p
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ ∀ᶠ (m : (ι × ι) × α) in (p'' ×ˢ p'') ×ˢ p', (F m.1.1 m.2, F m.1.2 m.2) ∈ u

Tactic:
have := (hf u hu).filter_mono (p'.prod_mono_left (Filter.prod_mono hp hp))

Result:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
p : Filter ι
p' : Filter α
p'' : Filter ι
hf : UniformCauchySeqOnFilter F p p'
hp : p'' ≤ p
u : Set (β × β)
hu : u ∈ 𝓤 β
this : ∀ᶠ (x : (ι × ι) × α) in (p'' ×ˢ p'') ×ˢ p', (F x.1.1 x.2, F x.1.2 x.2) ∈ u
⊢ ∀ᶠ (m : (ι × ι) × α) in (p'' ×ˢ p'') ×ˢ p', (F m.1.1 m.2, F m.1.2 m.2) ∈ u

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
p : Filter ι
p' : Filter α
p'' : Filter ι
hf : UniformCauchySeqOnFilter F p p'
hp : p'' ≤ p
u : Set (β × β)
hu : u ∈ 𝓤 β
this : ∀ᶠ (x : (ι × ι) × α) in (p'' ×ˢ p'') ×ˢ p', (F x.1.1 x.2, F x.1.2 x.2) ∈ u
⊢ ∀ (x : (ι × ι) × α), (F x.1.1 x.2, F x.1.2 x.2) ∈ u → (F x.1.1 x.2, F x.1.2 x.2) ∈ u

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Ideal/Lattice.lean
theorem eq_top_of_unit_mem (x y : α) (hx : x ∈ I) (h : y * x = 1) : I = ⊤ :=
  eq_top_iff.2 fun z _ =>
    calc
      z * y * x ∈ I := I.mul_mem_left _ hx
      _ = z * (y * x) := mul_assoc z y x
      _ = z

Proof state:
α : Type u
inst✝ : Semiring α
I : Ideal α
x y : α
hx : x ∈ I
h : y * x = 1
z : α
x✝ : z ∈ ⊤
⊢ z * (y * x) = z

Tactic:
rw [h, mul_one]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean
theorem left_vsub_lineMap (p₀ p₁ : P1) (c : k) : p₀ -ᵥ lineMap p₀ p₁ c = c • (p₀ -ᵥ p₁)

Proof state:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V1
inst✝¹ : Module k V1
inst✝ : AffineSpace V1 P1
p₀ p₁ : P1
c : k
⊢ p₀ -ᵥ (lineMap p₀ p₁) c = c • (p₀ -ᵥ p₁)

Tactic:
rw [← neg_vsub_eq_vsub_rev, lineMap_vsub_left, ← smul_neg, neg_vsub_eq_vsub_rev]

Result:
no goals
-- Mathlib/RingTheory/Adjoin/FG.lean
theorem fg_of_fg_toSubmodule {S : Subalgebra R A} : S.toSubmodule.FG → S.FG :=
  fun ⟨t, ht⟩ ↦ ⟨t, le_antisymm
    (Algebra.adjoin_le fun x hx ↦ show x ∈ Subalgebra.toSubmodule S from ht ▸ subset_span hx) <|
    show Subalgebra.toSubmodule S ≤ Subalgebra.toSubmodule (Algebra.adjoin R ↑t) from fun x hx ↦
      span_le.mpr (fun _ hx ↦ Algebra.subset_adjoin hx)
        (show x ∈ span R ↑t by
          rw [ht]
          exact hx)⟩

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
x✝ : (toSubmodule S).FG
t : Finset A
ht : span R ↑t = toSubmodule S
x : A
hx : x ∈ toSubmodule S
⊢ x ∈ span R ↑t

Tactic:
rw [ht]

Result:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
x✝ : (toSubmodule S).FG
t : Finset A
ht : span R ↑t = toSubmodule S
x : A
hx : x ∈ toSubmodule S
⊢ x ∈ toSubmodule S

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
x✝ : (toSubmodule S).FG
t : Finset A
ht : span R ↑t = toSubmodule S
x : A
hx : x ∈ toSubmodule S
⊢ x ∈ toSubmodule S

Tactic:
exact hx

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem le_inv_iff_mul_le : a ≤ b⁻¹ ↔ a * b ≤ 1

Proof state:
case ht
a b : ℝ≥0∞
⊢ b ≠ ⊤ ∨ 1 ≠ ⊤

Tactic:
right

Result:
case ht.h
a b : ℝ≥0∞
⊢ 1 ≠ ⊤

Proof state:
case ht.h
a b : ℝ≥0∞
⊢ 1 ≠ ⊤

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem Ideal.IsPrime.mem_pow_mul (I : Ideal R) [hI : I.IsPrime] {a b : R} {n : ℕ}
    (h : a * b ∈ I ^ n) : a ∈ I ^ n ∨ b ∈ I

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I.IsPrime
a b : R
n : ℕ
h : b * a ∈ I ^ n
⊢ b ∈ I ∨ a ∈ I ^ n

Tactic:
exact Ideal.IsPrime.mul_mem_pow _ h

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I.IsPrime
a b : R
n : ℕ
h : a * b ∈ I ^ n
⊢ a ∈ I ^ n ∨ b ∈ I

Tactic:
rw [mul_comm] at h

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I.IsPrime
a b : R
n : ℕ
h : b * a ∈ I ^ n
⊢ a ∈ I ^ n ∨ b ∈ I

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I.IsPrime
a b : R
n : ℕ
h : b * a ∈ I ^ n
⊢ a ∈ I ^ n ∨ b ∈ I

Tactic:
rw [or_comm]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I.IsPrime
a b : R
n : ℕ
h : b * a ∈ I ^ n
⊢ b ∈ I ∨ a ∈ I ^ n