mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f g : r ≺i s
a : α
⊢ f.toRelEmbedding a = g.toRelEmbedding a

Tactic:
rw [Subsingleton.elim f g]

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
hc : ↑c ⊆ bot x f
⊢ cSup c ∈ bot x f

Tactic:
s

Goal state after:
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
hc : ↑c ⊆ bot x f
s : Set α
⊢ s ∈ {s | IsAdmissible x f s} → cSup c ∈ s
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
a✝ : ωSup c ≤ x
i✝ : ℕ
⊢ c i✝ ≤ ωSup c

pp: α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
a✝ : ωSup c ≤ x
i✝ : ℕ
⊢ ωSup c ≤ x

Tactic:
· exact le_ωSup _ _

Goal state after:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
a✝ : ωSup c ≤ x
i✝ : ℕ
⊢ ωSup c ≤ x
Module: Mathlib.Order.Zorn

Goal state before:
pp: case refine_1.inl
α : Type u_1
inst✝ : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
x : α
hxs : x ∈ s
hcs : ∅ ⊆ {y | y ∈ s ∧ x ≤ y}
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) ∅
⊢ ∃ ub ∈ {y | y ∈ s ∧ x ≤ y}, ∀ z ∈ ∅, z ≤ ub

pp: case refine_1.inr
α : Type u_1
inst✝ : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
x : α
hxs : x ∈ s
c : Set α
hcs : c ⊆ {y | y ∈ s ∧ x ≤ y}
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
y : α
hy : y ∈ c
⊢ ∃ ub ∈ {y | y ∈ s ∧ x ≤ y}, ∀ z ∈ c, z ≤ ub

Tactic:
· exact ⟨x, ⟨hxs, le_rfl⟩, fun z => False.elim⟩

Goal state after:
case refine_1.inr
α : Type u_1
inst✝ : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
x : α
hxs : x ∈ s
c : Set α
hcs : c ⊆ {y | y ∈ s ∧ x ≤ y}
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
y : α
hy : y ∈ c
⊢ ∃ ub ∈ {y | y ∈ s ∧ x ≤ y}, ∀ z ∈ c, z ≤ ub
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case mp
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
c₀ : Chain (α →𝒄 β)
c₁ : Chain α
z : β
h : ∀ (i j : ℕ), (c₀ i) (c₁ j) ≤ z
i : ℕ
⊢ (c₀ i) (c₁ i) ≤ z

pp: case mpr
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
c₀ : Chain (α →𝒄 β)
c₁ : Chain α
z : β
h : ∀ (i : ℕ), (c₀ i) (c₁ i) ≤ z
i j : ℕ
⊢ (c₀ i) (c₁ j) ≤ z

Tactic:
· apply h

Goal state after:
case mpr
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
c₀ : Chain (α →𝒄 β)
c₁ : Chain α
z : β
h : ∀ (i : ℕ), (c₀ i) (c₁ i) ≤ z
i j : ℕ
⊢ (c₀ i) (c₁ j) ≤ z
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: a : Cardinal.{u_1}
⊢ lift.{v, u_1} (2 ^ a) = 2 ^ lift.{v, u_1} a

Tactic:
by
  simp [← one_add_one_eq_two]

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β✝ : Type u_3
γ✝ : Type u_4
δ : Type u_5
inst✝³ : OmegaCompletePartialOrder α
inst✝² : OmegaCompletePartialOrder β✝
inst✝¹ : OmegaCompletePartialOrder γ✝
inst✝ : OmegaCompletePartialOrder δ
β γ : Type v
f : α →𝒄 Part β
g : α →𝒄 β → Part γ
c : Chain α
⊢ ((↑f).partBind g.toOrderHom).toFun (ωSup c) = ωSup (c.map ((↑f).partBind g.toOrderHom))

Tactic:
rw [ωSup_bind, ← f.continuous, g.toOrderHom_eq_coe, ← g.continuous]

Goal state after:
ι : Sort u_1
α : Type u_2
β✝ : Type u_3
γ✝ : Type u_4
δ : Type u_5
inst✝³ : OmegaCompletePartialOrder α
inst✝² : OmegaCompletePartialOrder β✝
inst✝¹ : OmegaCompletePartialOrder γ✝
inst✝ : OmegaCompletePartialOrder δ
β γ : Type v
f : α →𝒄 Part β
g : α →𝒄 β → Part γ
c : Chain α
⊢ ((↑f).partBind ↑g).toFun (ωSup c) = f (ωSup c) >>= g (ωSup c)
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
⊢ ωSup (iterateChain (↑f) x h) ∈ fixedPoints ⇑f

Tactic:
mem_fixedPoints,

Goal state after:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
⊢ IsFixedPt (⇑f) (ωSup (iterateChain (↑f) x h))
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: a b : Cardinal.{u_1}
hb : 1 < b
⊢ a < b ^ a

Tactic:
rw [← succ_le_iff, (by norm_cast : succ (1 : Cardinal) = 2)] at hb

Goal state after:
a b : Cardinal.{u_1}
hb : 2 ≤ b
⊢ a < b ^ a
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case neg
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : a ≠ 0
hb : b ≠ 0
⊢ a < ℵ₀ ∧ b < ℵ₀

Tactic:
← Cardinal.one_le_iff_ne_zero

Goal state after:
case neg
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : 1 ≤ a
hb : 1 ≤ b
⊢ a < ℵ₀ ∧ b < ℵ₀
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case neg.right
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : 1 ≤ a
hb : 1 ≤ b
⊢ b < ℵ₀

Tactic:
· rw [← one_mul b]
      exact (mul_le_mul' ha le_rfl).trans_lt h

Goal state after:
Module: Mathlib.Algebra.Ring.Opposite

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ op ↑0 = 0

Tactic:
Nat.cast_zero,

Goal state after:
R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ op 0 = 0
Module: Mathlib.Algebra.Ring.Opposite

Goal state before:
pp: R : Type u_1
inst✝ : AddCommMonoidWithOne R
⊢ op ↑0 = 0

Tactic:
Nat.cast_zero,

Goal state after:
R : Type u_1
inst✝ : AddCommMonoidWithOne R
⊢ op 0 = 0
Module: Mathlib.GroupTheory.GroupAction.SubMulAction

Goal state before:
pp: S : Type u_1
R : Type u_2
M : Type u_3
inst✝³ : SetLike S M
inst✝² : Monoid R
inst✝¹ : MulAction R M
inst✝ : SMulMemClass S R M
s : S
r : Rˣ
⊢ r • ↑s = ↑s

Tactic:
by
  apply subset_antisymm (smul_subset_self _ s)
  rintro x hx
  exact ⟨r⁻¹ • x, SMulMemClass.smul_mem (↑r⁻¹ : R) hx, by simp [← Units.smul_def]⟩

Goal state after:
Module: Mathlib.Algebra.Ring.CharZero

Goal state before:
pp: α : Type u_1
R : Type u_2
S : Type u_3
n : ℕ
inst✝¹ : AddMonoidWithOne R
inst✝ : CharZero R
⊢ 2 ≠ 0

Tactic:
by rw [← Nat.cast_two, Nat.cast_ne_zero]; decide

Goal state after:
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: case zero
M : Type u_1
inst✝ : NonAssocSemiring M
x✝¹ x✝ : M
⊢ ↑0 * (x✝¹ * x✝) = ↑0 * x✝¹ * x✝

Tactic:
Nat.cast_zero,

Goal state after:
case zero
M : Type u_1
inst✝ : NonAssocSemiring M
x✝¹ x✝ : M
⊢ 0 * (x✝¹ * x✝) = 0 * x✝¹ * x✝
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: case zero
M : Type u_1
inst✝ : NonAssocSemiring M
x✝¹ x✝ : M
⊢ x✝¹ * x✝ * ↑0 = x✝¹ * (x✝ * ↑0)

Tactic:
Nat.cast_zero,

Goal state after:
case zero
M : Type u_1
inst✝ : NonAssocSemiring M
x✝¹ x✝ : M
⊢ x✝¹ * x✝ * 0 = x✝¹ * (x✝ * 0)
Module: Mathlib.Algebra.Group.Subsemigroup.Membership

Goal state before:
pp: ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
C : M → Prop
x₁ : M
hx₁ : x₁ ∈ ⨆ i, S i
mem : ∀ (i : ι), ∀ x₂ ∈ S i, C x₂
mul : ∀ (x y : M), C x → C y → C (x * y)
⊢ C x₁

Tactic:
by
  rw [iSup_eq_closure] at hx₁
  refine closure_induction (fun x₂ hx₂ => ?_) (fun x y _ _ ↦ mul x y) hx₁
  obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hx₂
  exact mem _ _ hi

Goal state after:
Module: Mathlib.Algebra.Prime.Defs

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
a✝ : M
irr : Irreducible a✝
primal : IsPrimal a✝
a b : M
dvd : a✝ ∣ a * b
⊢ a✝ ∣ a ∨ a✝ ∣ b

Tactic:
obtain ⟨d₁, d₂, h₁, h₂, rfl⟩ := primal dvd
    exact (of_irreducible_mul irr).symm.imp (·.mul_right_dvd.mpr h₁) (·.mul_left_dvd.mpr h₂)

Goal state after:
Module: Mathlib.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A₁
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₁
inst✝ : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
y : R
x : A₁
h : (algebraMap R A₂) y = e x
⊢ (algebraMap R A₁) y = x

Tactic:
by simpa using e.symm.toAlgHom.algebraMap_eq_apply h

Goal state after:
Module: Mathlib.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
this : IsLocalHom e.toRingEquiv
⊢ IsLocalHom ↑e

Tactic:
exact ⟨this.map_nonunit⟩

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Pointwise

Goal state before:
pp: case le
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
N : Submodule R M
inst✝ : SMulCommClass S R M
r : S
⊢ r • N ≤ {r} • N

Tactic:
rintro _ ⟨m, hm, rfl⟩

Goal state after:
case le
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
N : Submodule R M
inst✝ : SMulCommClass S R M
r : S
m : M
hm : m ∈ ↑N
⊢ (DistribSMul.toLinearMap R M r) m ∈ {r} • N
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ span R 0 = ⊥

Tactic:
by rw [← singleton_zero, span_singleton_eq_bot]

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: ι : Sort u_1
α : Type u_3
inst✝² : ConditionallyCompleteLattice α
f : ι → α
s : Set α
inst✝¹ : Finite ι
inst✝ : Nonempty ι
hs : SupClosed s
hf : ∀ (i : ι), f i ∈ s
⊢ ⨆ i, f i ∈ s

Tactic:
cases nonempty_fintype (PLift ι)
  rw [← iSup_plift_down, ← Finset.sup'_univ_eq_ciSup]
  exact hs.finsetSup'_mem Finset.univ_nonempty fun _ _ ↦ hf _

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
u v : Finset ι
hs : s.SupIndep f
hu : u ⊆ s
hv : v ⊆ s
huv : Disjoint u v
⊢ Disjoint (u.sup f) (v.sup f)

Tactic:
classical
  induction u using Finset.induction generalizing v with
  | empty => simp
  | insert x u hx ih =>
    grind [= SupIndep, Disjoint.disjoint_sup_left_of_disjoint_sup_right]

Goal state after:
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case mp
α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : IsCompactElement k
⊢ ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x

Tactic:
s

Goal state after:
case mp
α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : IsCompactElement k
s : Set α
⊢ s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
⊢ IsCompactElement k

Tactic:
s

Goal state after:
case mpr
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
⊢ ∀ (u : α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → IsLUB s u → k ≤ u → ∃ x ∈ s, k ≤ x
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case mp
α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
⊢ ∀ (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id

Tactic:
s

Goal state after:
case mp
α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
⊢ k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
β : ι → Type u_5
t : (i : ι) → β i → α
ht : ∀ (i : ι), iSupIndep (t i)
b₁ : (i : ι) → β i
hb₁ : b₁ ∈ {b | ⨅ i, t i (b i) ≠ ⊥}
b₂ : (i : ι) → β i
hb₂ : b₂ ∈ {b | ⨅ i, t i (b i) ≠ ⊥}
⊢ (fun b ↦ ⨅ i, t i (b i)) b₁ = (fun b ↦ ⨅ i, t i (b i)) b₂ → b₁ = b₂

Tactic:
h_eq

Goal state after:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
β : ι → Type u_5
t : (i : ι) → β i → α
ht : ∀ (i : ι), iSupIndep (t i)
b₁ : (i : ι) → β i
hb₁ : b₁ ∈ {b | ⨅ i, t i (b i) ≠ ⊥}
b₂ : (i : ι) → β i
hb₂ : b₂ ∈ {b | ⨅ i, t i (b i) ≠ ⊥}
h_eq : (fun b ↦ ⨅ i, t i (b i)) b₁ = (fun b ↦ ⨅ i, t i (b i)) b₂
⊢ b₁ = b₂
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case mp
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
i j : ι
hij : i ≠ j
huniv : ∀ (k : ι), k = i ∨ k = j
⊢ iSupIndep t → Disjoint (t i) (t j)

pp: case mpr
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
i j : ι
hij : i ≠ j
huniv : ∀ (k : ι), k = i ∨ k = j
⊢ Disjoint (t i) (t j) → iSupIndep t

Tactic:
· exact fun h => h.pairwiseDisjoint hij

Goal state after:
case mpr
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
i j : ι
hij : i ≠ j
huniv : ∀ (k : ι), k = i ∨ k = j
⊢ Disjoint (t i) (t j) → iSupIndep t
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
⊢ ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x

Tactic:
s

Goal state after:
case mpr
α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
s : Set α
⊢ s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case mp
α : Type u
inst✝ : CompleteLattice α
k : α
H : ∀ (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
ι : Type u
⊢ ∀ (s : ι → α), k ≤ iSup s → ∃ t, k ≤ t.sup s

Tactic:
s

Goal state after:
case mp
α : Type u
inst✝ : CompleteLattice α
k : α
H : ∀ (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
ι : Type u
s : ι → α
⊢ k ≤ iSup s → ∃ t, k ≤ t.sup s
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case mpr
α : Type u
inst✝ : CompleteLattice α
k : α
H : ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t, k ≤ t.sup s
⊢ ∀ (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id

Tactic:
s

Goal state after:
case mpr
α : Type u
inst✝ : CompleteLattice α
k : α
H : ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t, k ≤ t.sup s
s : Set α
⊢ k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
Module: Mathlib.Algebra.Algebra.Tower

Goal state before:
pp: R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
t : Set A
k : S
hks : k ∈ span R s
x : A
hx : x ∈ t
c₁ c₂ : S
x✝¹ : c₁ ∈ span R s
x✝ : c₂ ∈ span R s
ih₁ : c₁ • x ∈ span R (s • t)
ih₂ : c₂ • x ∈ span R (s • t)
⊢ (c₁ + c₂) • x ∈ span R (s • t)

Tactic:
rw [add_smul]; exact add_mem ih₁ ih₂

Goal state after:
Module: Mathlib.Algebra.BigOperators.GroupWithZero.Finset

Goal state before:
pp: ι : Type u_1
G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
s : Finset ι
f : ι → G₀
h : ∏ i ∈ s, f i ≠ 0
⊢ mk0 (∏ i ∈ s, f i) h = ∏ i ∈ s.attach, mk0 (f ↑i) ⋯

Tactic:
by
  induction s using Finset.cons_induction_on <;> simp [*]

Goal state after:
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
⊢ ∀ (c : α), IsCompactElement c → c ≤ a ⊓ sSup s → c ≤ ⨆ b ∈ s, a ⊓ b

Tactic:
by_cases hs : s.Nonempty

Goal state after:
case pos
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hs : s.Nonempty
⊢ ∀ (c : α), IsCompactElement c → c ≤ a ⊓ sSup s → c ≤ ⨆ b ∈ s, a ⊓ b

case neg
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hs : ¬s.Nonempty
⊢ ∀ (c : α), IsCompactElement c → c ≤ a ⊓ sSup s → c ≤ ⨆ b ∈ s, a ⊓ b
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
s : Finset α
hs : ↑s ⊆ f '' {j | j ≠ i}
t : Finset α := s.erase ⊥
hf : InjOn f (f ⁻¹' ↑t)
this : Finset.image f ((insert i (t.preimage f hf)).erase i) = t
⊢ Disjoint (f i) (((insert i (t.preimage f hf)).erase i).sup (id ∘ f))

Tactic:
specialize h (insert i (t.preimage _ hf))

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
i : ι
s : Finset α
hs : ↑s ⊆ f '' {j | j ≠ i}
t : Finset α := s.erase ⊥
hf : InjOn f (f ⁻¹' ↑t)
h : (insert i (t.preimage f hf)).SupIndep f
this : Finset.image f ((insert i (t.preimage f hf)).erase i) = t
⊢ Disjoint (f i) (((insert i (t.preimage f hf)).erase i).sup (id ∘ f))
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
x : ↥p
⊢ map p.subtype (R ∙ x) = R ∙ ↑x

Tactic:
by simp [← span_image]

Goal state after:
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLattice α
h : WellFoundedGT α
⊢ IsCompactlyGenerated α

Tactic:
rw [wellFoundedGT_iff_isSupFiniteCompact, isSupFiniteCompact_iff_all_elements_compact] at h
  -- x is the join of the set of compact elements {x}
  exact ⟨fun x => ⟨{x}, ⟨fun x _ => h x, sSup_singleton⟩⟩⟩

Goal state after:
Module: Mathlib.Algebra.BigOperators.Ring.Multiset

Goal state before:
pp: M₀ : Type u_3
inst✝² : CommMonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
s : Multiset M₀
l : List M₀
⊢ prod ⟦l⟧ = 0 ↔ 0 ∈ ⟦l⟧

Tactic:
rw [quot_mk_to_coe, prod_coe]

Goal state after:
M₀ : Type u_3
inst✝² : CommMonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
s : Multiset M₀
l : List M₀
⊢ l.prod = 0 ↔ 0 ∈ ↑l
Module: Mathlib.Algebra.BigOperators.Ring.Multiset

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝ : NonUnitalNonAssocSemiring R
a : R
s✝ : Multiset ι
f : ι → R
i : ι
s : Multiset ι
ih : (map (fun i ↦ a * f i) s).sum = a * (map f s).sum
⊢ (map (fun i ↦ a * f i) (i ::ₘ s)).sum = a * (map f (i ::ₘ s)).sum

Tactic:
simp [ih, mul_add]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: R : Type u_4
inst✝ : NonUnitalNonAssocSemiring R
m n : ℕ
f g : ℕ → R
⊢ (∑ i ∈ range (m + 1), f i) * ∑ i ∈ range (n + 1), g i =
    (∑ i ∈ range m, f i) * ∑ i ∈ range n, g i + f m * ∑ i ∈ range n, g i + (∑ i ∈ range m, f i) * g n + f m * g n

Tactic:
simp only [add_mul, mul_add, add_assoc, sum_range_succ]

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective ⇑f
p : Submodule R₂ M₂
this : Injective (comap f)
⊢ (p ≠ ⊤ ∧ ∀ (b : Submodule R M), comap f p < b → b = comap f ⊤) ↔ p ≠ ⊤ ∧ ∀ (b : Submodule R₂ M₂), p < b → b = ⊤

Tactic:
refine and_congr_right fun _ ↦
    ⟨fun h m hm ↦ this (h _ <| comap_strictMono_of_surjective hf hm), fun h m hm ↦ ?_⟩

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective ⇑f
p : Submodule R₂ M₂
this : Injective (comap f)
x✝ : p ≠ ⊤
h : ∀ (b : Submodule R₂ M₂), p < b → b = ⊤
m : Submodule R M
hm : comap f p < m
⊢ m = comap f ⊤
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : LinearOrder ι
f g : ι → R
a : ι
⊢ ∀ (s : Finset ι),
    (∀ x ∈ s, x < a) →
      ∏ i ∈ s, (f i + g i) = ∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j →
        ∏ i ∈ insert a s, (f i + g i) =
          ∏ i ∈ insert a s, f i +
            ∑ i ∈ insert a s, (g i * ∏ j ∈ insert a s with j < i, (f j + g j)) * ∏ j ∈ insert a s with i < j, f j

Tactic:
s

Goal state after:
ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : LinearOrder ι
f g : ι → R
a : ι
s : Finset ι
⊢ (∀ x ∈ s, x < a) →
    ∏ i ∈ s, (f i + g i) = ∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j →
      ∏ i ∈ insert a s, (f i + g i) =
        ∏ i ∈ insert a s, f i +
          ∑ i ∈ insert a s, (g i * ∏ j ∈ insert a s with j < i, (f j + g j)) * ∏ j ∈ insert a s with i < j, f j
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.IsTorsionFree R M
x : M
h : x ≠ 0
⊢ (coord R M x h) ⟨x, ⋯⟩ = 1

Tactic:
← toSpanNonzeroSingleton_one R M x h,

Goal state after:
R : Type u_1
M : Type u_4
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.IsTorsionFree R M
x : M
h : x ≠ 0
⊢ (coord R M x h) ((toSpanNonzeroSingleton R M x h) 1) = 1
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hyf : y ∈ f.support
h : α
hx : h ∈ f.support.erase y
⊢ g h ((erase y f) h) = g h (f h)

Tactic:
rw [Finsupp.erase_ne (ne_of_mem_erase hx)]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: case refine_2
α : Type u_16
ι : Type u_17
M : Type u_18
inst✝¹ : DecidableEq α
inst✝ : AddCommMonoid M
g : ι → α →₀ M
s : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
i : ι
⊢ ∀ (s : Finset ι),
    i ∉ s →
      ((∑ i ∈ s, g i).support = s.biUnion fun i ↦ (g i).support) →
        (∑ i ∈ insert i s, g i).support = (insert i s).biUnion fun i ↦ (g i).support

Tactic:
s

Goal state after:
case refine_2
α : Type u_16
ι : Type u_17
M : Type u_18
inst✝¹ : DecidableEq α
inst✝ : AddCommMonoid M
g : ι → α →₀ M
s✝ : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
i : ι
s : Finset ι
⊢ i ∉ s →
    ((∑ i ∈ s, g i).support = s.biUnion fun i ↦ (g i).support) →
      (∑ i ∈ insert i s, g i).support = (insert i s).biUnion fun i ↦ (g i).support
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝⁴ : CommRing S
inst✝³ : PartialOrder S
inst✝² : IsOrderedRing S
inst✝¹ : Ring R
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a : R
⊢ abv (-a) = abv a

Tactic:
by_cases ha : a = 0; · simp [ha]
  refine
    (mul_self_eq_mul_self_iff.mp (by rw [← abv.map_mul, neg_mul_neg, abv.map_mul])).resolve_right ?_
  exact ((neg_lt_zero.mpr (abv.pos ha)).trans (abv.pos (neg_ne_zero.mpr ha))).ne'

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f1 f2 : α →₀ M
g1 g2 : α → M → N
h1 : f1.support ⊆ f2.support
h2 : ∀ a ∈ f1.support, g1 a (f1 a) ∣ g2 a (f2 a)
⊢ ∀ i ∈ f1.support, g1 i (f1 i) ∣ g2 i (f2 i)

Tactic:
exact h2

Goal state after:
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_12
M : Type u_13
inst✝ : Zero M
f g : α →₀ M
h : f.graph = g.graph
⊢ image Prod.fst g.graph = g.support

Tactic:
image_fst_graph

Goal state after:
α : Type u_12
M : Type u_13
inst✝ : Zero M
f g : α →₀ M
h : f.graph = g.graph
⊢ g.support = g.support
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case h₀
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
x : α →₀ M
a : α
⊢ ∀ (b : α), x b ≠ 0 → b ≠ a → (single (f b) (x b)) (f a) = 0

Tactic:
intro b _ hba
    exact single_eq_of_ne' (hf.ne hba)

Goal state after: