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

Goal state before:
pp: case succ
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddCommGroupWithOne α
inst✝ : PredSubOrder α
x : α
n : ℕ
IH : pred^[n] x = x - ↑n
⊢ pred^[n + 1] x = x - ↑(n + 1)

Tactic:
rw [Function.iterate_succ_apply', IH, Nat.cast_add, pred_eq_sub_one, Nat.cast_one, sub_sub]

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

Goal state before:
pp: m : ℕ∞
n : ℕ
hn : n ≠ 0
⊢ m.toNat = n ↔ m = ↑n

Tactic:
by
  induction m <;> simp [hn.symm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
n✝ n' m : ℕ
s✝ : Sym α n✝
a b : α
n : ℕ
inst✝ : IsEmpty α
s : Sym α n.succ
⊢ False

Tactic:
by
    obtain ⟨a, -⟩ := exists_mem s
    exact isEmptyElim a

Goal state after:
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: case mp
α : Type u
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
s : ℕ → α
hps : ∀ (n : ℕ), p (s n)
hs : ⨆ n, s n = ⊤
⊢ sSup (range s) = ⊤

Tactic:
sSup_range

Goal state after:
case mp
α : Type u
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
s : ℕ → α
hps : ∀ (n : ℕ), p (s n)
hs : ⨆ n, s n = ⊤
⊢ iSup s = ⊤
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case refine_2.inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
b✝ d✝ : β
hab : b✝ ≤ d✝
hba : ¬inr d✝ ≤ inr b✝
⊢ inr b✝ < inr d✝

Tactic:
· exact LiftRel.inr (hab.lt_of_not_ge fun h => hba <| LiftRel.inr h)

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Defs

Goal state before:
pp: ι : Type u_1
f : ι → Cardinal.{u_2}
⊢ prod f ≠ 0 ↔ ∀ (i : ι), f i ≠ 0

Tactic:
by simp [prod_eq_zero]

Goal state after:
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
D : Set (Set α)
f : α → β
g : β → γ
D' : Set (Set β)
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hD' : MapsTo (fun x ↦ f '' x) D D'
hg : ScottContinuousOn D' g
hf : ScottContinuousOn D f
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
ha : IsLUB d a
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (f '' d)

Tactic:
have := hf.monotone

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
D : Set (Set α)
f : α → β
g : β → γ
D' : Set (Set β)
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hD' : MapsTo (fun x ↦ f '' x) D D'
hg : ScottContinuousOn D' g
hf : ScottContinuousOn D f
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
ha : IsLUB d a
this : (∀ (a b : α), a ≤ b → {a, b} ∈ D) → Monotone f
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (f '' d)
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: β : Type u_2
inst✝ : SemilatticeSup β
d : Set (β × β)
x✝² : d.Nonempty
x✝¹ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
x✝ : β × β
p₁ p₂ : β
hdp : (∀ (a b : β), (a, b) ∈ d → a ≤ p₁ ∧ b ≤ p₂) ∧ (p₁, p₂) ∈ lowerBounds {x | ∀ (a b : β), (a, b) ∈ d → (a, b) ≤ x}
e1 : ∀ (a b : β), (∀ (b₁ b₂ : β), (b₁, b₂) ∈ d → b₁ ≤ a ∧ b₂ ≤ b) → p₁ ≤ a ∧ p₂ ≤ b
⊢ p₁ ⊔ p₂ ∈ {x | ∀ ⦃a : β⦄ (x_1 x_2 : β), (x_1, x_2) ∈ d → x_1 ⊔ x_2 = a → a ≤ x} ∧
    p₁ ⊔ p₂ ∈ lowerBounds {x | ∀ ⦃a : β⦄ (x_1 x_2 : β), (x_1, x_2) ∈ d → x_1 ⊔ x_2 = a → a ≤ x}

Tactic:
refine ⟨fun a b₁ b₂ hbd hba => ?_,fun b hb => ?_⟩

Goal state after:
case refine_1
β : Type u_2
inst✝ : SemilatticeSup β
d : Set (β × β)
x✝² : d.Nonempty
x✝¹ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
x✝ : β × β
p₁ p₂ : β
hdp : (∀ (a b : β), (a, b) ∈ d → a ≤ p₁ ∧ b ≤ p₂) ∧ (p₁, p₂) ∈ lowerBounds {x | ∀ (a b : β), (a, b) ∈ d → (a, b) ≤ x}
e1 : ∀ (a b : β), (∀ (b₁ b₂ : β), (b₁, b₂) ∈ d → b₁ ≤ a ∧ b₂ ≤ b) → p₁ ≤ a ∧ p₂ ≤ b
a b₁ b₂ : β
hbd : (b₁, b₂) ∈ d
hba : b₁ ⊔ b₂ = a
⊢ a ≤ p₁ ⊔ p₂

case refine_2
β : Type u_2
inst✝ : SemilatticeSup β
d : Set (β × β)
x✝² : d.Nonempty
x✝¹ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
x✝ : β × β
p₁ p₂ : β
hdp : (∀ (a b : β), (a, b) ∈ d → a ≤ p₁ ∧ b ≤ p₂) ∧ (p₁, p₂) ∈ lowerBounds {x | ∀ (a b : β), (a, b) ∈ d → (a, b) ≤ x}
e1 : ∀ (a b : β), (∀ (b₁ b₂ : β), (b₁, b₂) ∈ d → b₁ ≤ a ∧ b₂ ≤ b) → p₁ ≤ a ∧ p₂ ≤ b
b : β
hb : b ∈ {x | ∀ ⦃a : β⦄ (x_1 x_2 : β), (x_1, x_2) ∈ d → x_1 ⊔ x_2 = a → a ≤ x}
⊢ p₁ ⊔ p₂ ≤ b
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
o : Part α
inst✝ : Decidable o.Dom
⊢ o.toOption.isSome = true ↔ o.Dom

Tactic:
by
  by_cases h : o.Dom <;> simp [h, toOption]

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
o : Part α
inst✝ : Decidable o.Dom
⊢ o.toOption = none ↔ ¬o.Dom

Tactic:
by
  by_cases h : o.Dom <;> simp [h, toOption]

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
s : Set α
hs : s ∈ {s | IsAdmissible x f s}
⊢ cSup c ∈ s

Tactic:
exact hs.cSup_mem c (subset_trans hc (sInter_subset_of_mem hs))

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_4
f : α → β
x : Part α
g : β → Part γ
⊢ (x.bind fun y ↦ some (f y)).bind g = x.bind fun y ↦ g (f y)

Tactic:
bind_assoc

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_4
f : α → β
x : Part α
g : β → Part γ
⊢ (x.bind fun x ↦ (some (f x)).bind g) = x.bind fun y ↦ g (f y)
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_4
f : α → Part β
x : Part α
g : β → γ
⊢ ((x.bind f).bind fun y ↦ some (g y)) = x.bind fun y ↦ map g (f y)

Tactic:
bind_assoc

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_4
f : α → Part β
x : Part α
g : β → γ
⊢ (x.bind fun x ↦ (f x).bind fun y ↦ some (g y)) = x.bind fun y ↦ map g (f y)
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case image_self_subset_self
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : y ∈ {y | IsExtremePt x f y}
z : α
hz : z ∈ bot x f
hzy : z < f y
hz' : z ∈ bot x f
⊢ f z ≤ f y

Tactic:
← bot_eq_of_le_or_map_le le_map hy

Goal state after:
case image_self_subset_self
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : y ∈ {y | IsExtremePt x f y}
z : α
hz : z ∈ bot x f
hzy : z < f y
hz' : z ∈ {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}
⊢ f z ≤ f y
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
c : Chain (Part α)
x : Part α
hx : ∀ (i : ℕ), c i ≤ x
a : α
ha : a ∈ Part.ωSup c
⊢ a ∈ x

Tactic:
replace ha := mem_chain_of_mem_ωSup ha

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
c : Chain (Part α)
x : Part α
hx : ∀ (i : ℕ), c i ≤ x
a : α
ha : some a ∈ c
⊢ a ∈ x
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
⊢ y ∈ bot x f ↔ IsExtremePt x f y

Tactic:
rw [← setOfPred_isExtremePt_eq_bot le_map, mem_ofPred]

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : IsExtremePt x f y
z : α
hz : z ∈ bot x f
a✝ : y ≠ z
⊢ (fun x1 x2 ↦ x1 ≤ x2) y z ∨ (fun x1 x2 ↦ x1 ≤ x2) z y

Tactic:
← bot_eq_of_le_or_map_le le_map hy

Goal state after:
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : IsExtremePt x f y
z : α
hz : z ∈ {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}
a✝ : y ≠ z
⊢ (fun x1 x2 ↦ x1 ≤ x2) y z ∨ (fun x1 x2 ↦ x1 ≤ x2) z y
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: α β : Type u
a b : ℕ
h : Fintype.card (Fin a) = Fintype.card (Fin b)
⊢ a = b

Tactic:
Fintype.card_fin,

Goal state after:
α β : Type u
a b : ℕ
h : a = Fintype.card (Fin b)
⊢ a = b
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: c : Cardinal.{0}
h' : c < #ℕ
h : lift.{u_1, 0} c < ℵ₀
⊢ ∃ n, lift.{u_1, 0} c = ↑n

Tactic:
rcases le_mk_iff_exists_set.1 h'.1 with ⟨S, rfl⟩

Goal state after:
S : Set ℕ
h' : #↑S < #ℕ
h : lift.{u_1, 0} #↑S < ℵ₀
⊢ ∃ n, lift.{u_1, 0} #↑S = ↑n
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: n : ℕ
h : ∀ (n_1 : ℕ), ↑n_1 ≤ ↑n
hn : ↑n < ℵ₀
⊢ False

Tactic:
exact (Nat.lt_succ_self _).not_ge (Nat.cast_le.1 (h (n + 1)))

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: c : Cardinal.{u_1}
h : IsSuccLimit c
⊢ ℵ₀ ≤ c

Tactic:
contrapose! h
  exact not_isSuccLimit_of_lt_aleph0 h

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Free

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
r : R
m : M
inst✝¹ : IsTorsionFree R M
inst✝ : IsCancelMulZero R
⊢ r • m = 0 ↔ r = 0 ∨ m = 0

Tactic:
obtain rfl | hr := eq_or_ne r 0

Goal state after:
case inl
R : Type u_1
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
m : M
inst✝¹ : IsTorsionFree R M
inst✝ : IsCancelMulZero R
⊢ 0 • m = 0 ↔ 0 = 0 ∨ m = 0

case inr
R : Type u_1
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
r : R
m : M
inst✝¹ : IsTorsionFree R M
inst✝ : IsCancelMulZero R
hr : r ≠ 0
⊢ r • m = 0 ↔ r = 0 ∨ m = 0
Module: Mathlib.Algebra.GroupWithZero.Action.Prod

Goal state before:
pp: case e_4.e_2
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : AddMonoid α
fst✝ : DistribMulAction M α
x : DistribMulAction N α
snd✝ : SMulCommClass M N α
⊢ (fun x_1 ↦ SMulCommClass M N α) = fun x ↦ SMulCommClass M N α

Tactic:
funext i; congr; ext m a; clear i; (conv_rhs => rw [← one_smul N a]); rfl

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

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : M →ₗ[R] M
h : Commute f g
⊢ f.ker ≤ (g ∘ₗ f).ker

Tactic:
exact ker_le_ker_comp f g

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

Goal state before:
pp: R : Type u
M : Type v
N : Type w
inst✝¹ : AddZeroClass M
inst✝ : DistribSMul R M
c : R
f g : ULift.{?u.13, v} M
⊢ c • (f + g) = c • f + c • g

Tactic:
by
    ext
    simp [smul_add]

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

Goal state before:
pp: R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
n : ℕ
a b : R
h : ↑n * a = ↑n * b
w : n ≠ 0
⊢ a = b

Tactic:
by
  simpa [w] using nat_mul_inj h

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

Goal state before:
pp: case mpr
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M
inst✝² : Module R₂ M₂
τ₁₂ : R →+* R₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
p : Submodule R M
e : M ≃ₛₗ[τ₁₂] M₂
x : M₂
⊢ e.symm x ∈ p → ∃ y ∈ p, ↑e y = x

Tactic:
intro hx
    exact ⟨e.symm x, hx, by simp⟩

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

Goal state before:
pp: M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ -(↑n * x✝¹ * x✝) = -(↑n * x✝¹) * x✝

Tactic:
neg_mul

Goal state after:
M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ -(↑n * x✝¹ * x✝) = -(↑n * x✝¹ * x✝)
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ x✝¹ * x✝ * (-1 + -↑n) = x✝¹ * (x✝ * (-1 + -↑n))

Tactic:
rw [mul_add, mul_add, mul_add, mul_neg, mul_one, mul_neg, mul_neg, mul_one, mul_neg,
          add_right_inj, (natCast_mem_center _ n).right_assoc _ _, mul_neg, mul_neg]

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

Goal state before:
pp: M : Type u_1
inst✝ : NonUnitalNonAssocRing M
a : M
ha : a ∈ center M
x✝¹ x✝ : M
⊢ -(a * x✝¹ * x✝) = -(a * x✝¹) * x✝

Tactic:
neg_mul

Goal state after:
M : Type u_1
inst✝ : NonUnitalNonAssocRing M
a : M
ha : a ∈ center M
x✝¹ x✝ : M
⊢ -(a * x✝¹ * x✝) = -(a * x✝¹ * x✝)
Module: Mathlib.Algebra.Ring.Centralizer

Goal state before:
pp: M : Type u_1
S : Set M
a : M
inst✝¹ : Mul M
inst✝ : HasDistribNeg M
ha : a ∈ S.centralizer
c : M
hc : c ∈ S
⊢ -(a * c) = -a * c

Tactic:
neg_mul

Goal state after:
M : Type u_1
S : Set M
a : M
inst✝¹ : Mul M
inst✝ : HasDistribNeg M
ha : a ∈ S.centralizer
c : M
hc : c ∈ S
⊢ -(a * c) = -(a * c)
Module: Mathlib.Algebra.Algebra.Hom

Goal state before:
pp: R : Type u
A : Type v
B : Type w
C : Type u₁
D : Type v₁
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Semiring C
inst✝⁴ : Semiring D
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra R C
inst✝ : Algebra R D
φ : A →ₐ[R] B
f : A →ₗ[R] B
map_one : f 1 = 1
map_mul : ∀ (x y : A), f (x * y) = f x * f y
c : R
⊢ f ((algebraMap R A) c) = (algebraMap R B) c

Tactic:
by simp only [Algebra.algebraMap_eq_smul_one, f.map_smul, map_one]

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Lemmas

Goal state before:
pp: case mp.refine_1
M : Type u_2
inst✝ : Monoid M
x y : M
h : Irreducible (x * y)
h' : IsUnit y
⊢ Irreducible x

Tactic:
irreducible_mul_isUnit h'

Goal state after:
case mp.refine_1
M : Type u_2
inst✝ : Monoid M
x y : M
h : Irreducible x
h' : IsUnit y
⊢ Irreducible x
Module: Mathlib.Algebra.Prime.Lemmas

Goal state before:
pp: case inr
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : M
hp : Prime p
a b x : M
hc : b = a * x
⊢ p ∣ a ∨ a ∣ b

Tactic:
exact Or.inr (hc.symm ▸ dvd_mul_right _ _)

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

Goal state before:
pp: 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
inst✝ : SMulCommClass S R M
s : Set S
N : Submodule R M
⊢ {p | ∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p} = {x | ⨆ a ∈ s, a • N ≤ x}

Tactic:
iSup_le_iff,

Goal state after:
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
inst✝ : SMulCommClass S R M
s : Set S
N : Submodule R M
⊢ {p | ∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p} = {x | ∀ i ∈ s, i • N ≤ x}
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsModularLattice α
a b c : α
h₀ : Codisjoint a b
h₁ : Disjoint b c
h₂ : a ≤ c
⊢ c ≤ a

Tactic:
by simpa [h₀.eq_top, h₁.eq_bot] using sup_inf_le_assoc_of_le b h₂

Goal state after:
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
p p' : Submodule R M
⊢ ↑(p ⊔ p') = ↑p + ↑p'

Tactic:
by
  ext
  rw [SetLike.mem_coe, mem_sup, Set.mem_add]
  simp

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_4
inst✝¹ : Preorder α
inst✝ : IsStronglyAtomic α
s : Set α
h : s.OrdConnected
⊢ ∀ (a b : ↑s), a < b → ∃ x, a ⋖ x ∧ x ≤ b

Tactic:
rintro ⟨c, hc⟩ ⟨d, hd⟩ hcd
    obtain ⟨x, hcx, hxd⟩ := (Subtype.mk_lt_mk.1 hcd).exists_covby_le
    exact ⟨⟨x, h.out' hc hd ⟨hcx.le, hxd⟩⟩,
      ⟨by simpa
        using! hcx.lt, fun y hy hy' ↦ hcx.2 (by simpa using! hy) (by simpa using! hy')⟩, hxd⟩

Goal state after:
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
S : Type u_9
inst✝² : SMul S R
inst✝¹ : SMul S M
inst✝ : IsScalarTower S R M
r : S
x : M
⊢ r • x ∈ R ∙ x

Tactic:
exact smul_of_tower_mem _ _ (mem_span_singleton_self _)

Goal state after:
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
x y z : M
hxy : {x} ⊆ ↑(R ∙ y)
hyz : {y} ⊆ ↑(R ∙ z)
⊢ {x} ⊆ ↑(R ∙ z)

Tactic:
exact Submodule.subset_span_trans hxy hyz

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

Goal state before:
pp: case refine_1.refine_2
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set M
x✝ : M
hx✝ : x✝ ∈ span R S
x : M
hx : x ∈ S
⊢ x ∈ span R ↑{x}

Tactic:
rw [Finset.coe_singleton]
      exact Submodule.mem_span_singleton_self x

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

Goal state before:
pp: case insert
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
a : M
t : Finset M
hat : a ∉ t
IH : ↑t ⊆ ↑(span R s) → ∃ T, ↑T ⊆ s ∧ ↑t ⊆ ↑(span R ↑T)
ht : ↑(insert a t) ⊆ ↑(span R s)
T : Finset M
hTs : ↑T ⊆ s
htT : ↑t ⊆ ↑(span R ↑T)
⊢ ∃ T, ↑T ⊆ s ∧ ↑(insert a t) ⊆ ↑(span R ↑T)

Tactic:
obtain ⟨T', hT's, haT'⟩ := mem_span_finite_of_mem_span (ht (Finset.mem_insert_self _ _))

Goal state after:
case insert
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
a : M
t : Finset M
hat : a ∉ t
IH : ↑t ⊆ ↑(span R s) → ∃ T, ↑T ⊆ s ∧ ↑t ⊆ ↑(span R ↑T)
ht : ↑(insert a t) ⊆ ↑(span R s)
T : Finset M
hTs : ↑T ⊆ s
htT : ↑t ⊆ ↑(span R ↑T)
T' : Finset M
hT's : ↑T' ⊆ s
haT' : a ∈ span R ↑T'
⊢ ∃ T, ↑T ⊆ s ∧ ↑(insert a t) ⊆ ↑(span R ↑T)
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
ht : iSupIndep t
⊢ sSupIndep (range t)

Tactic:
sSupIndep_iff

Goal state after:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
ht : iSupIndep t
⊢ iSupIndep Subtype.val
Module: Mathlib.Algebra.Notation.Indicator

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f : α → M
⊢ (s ∩ mulSupport f).mulIndicator f = s.mulIndicator f

Tactic:
rw [← mulIndicator_mulIndicator, mulIndicator_mulSupport]

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

Goal state before:
pp: case refine_2
α : Type u_2
inst✝ : CompleteLattice α
h : ∀ (k : α) (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
s : Set α
⊢ ∃ t, ↑t ⊆ s ∧ sSup s = t.sup id

Tactic:
· obtain ⟨t, ⟨hts, htsup⟩⟩ := h (sSup s) s (by rfl)
    have : sSup s = t.sup id := by
      suffices t.sup id ≤ sSup s by apply le_antisymm <;> assumption
      simp only [id, Finset.sup_le_iff]
      intro x hx
      exact le_sSup (hts hx)
    exact ⟨t, hts, this⟩

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

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝² : CommMonoidWithZero M₀
f : ι → M₀
s : Finset ι
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
x✝ : ∃ a ∈ ∅, f a = 0
w✝ : ι
H : w✝ ∈ ∅
right✝ : f w✝ = 0
⊢ ∏ x ∈ ∅, f x = 0

Tactic:
simp at H

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

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
V : Submodule R M
f g : ↥V →ₗ[R] N
S : Set M
hV : V = span R S
⊢ (∀ (s : ↑S), f ⟨↑s, ⋯⟩ = g ⟨↑s, ⋯⟩) → f = g

Tactic:
· intro h
    subst hV
    suffices ∀ (x : M) (hx : x ∈ span R S), f ⟨x, hx⟩ = g ⟨x, hx⟩ by
      ext ⟨x, hx⟩
      exact this x hx
    intro x hx
    induction hx using span_induction with
    | mem x hx => exact h ⟨x, hx⟩
    | zero => erw [map_zero, map_zero]
    | add x y hx hy hx' hy' =>
        erw [f.map_add ⟨x, hx⟩ ⟨y, hy⟩, g.map_add ⟨x, hx⟩ ⟨y, hy⟩]
        rw [hx', hy']
    | smul a x hx hx' =>
        erw [f.map_smul a ⟨x, hx⟩, g.map_smul a ⟨x, hx⟩]
        rw [hx']

Goal state after:
Module: Mathlib.Algebra.BigOperators.Pi

Goal state before:
pp: ι : Type u_1
κ : Type u_2
R : Type u_5
inst✝ : CommSemiring R
s : Finset ι
f : ι → Set κ
g : ι → κ → R
j : κ
⊢ ∏ i ∈ s, (f i).indicator (g i) j = if j ∈ ⋂ x ∈ s, f x then (∏ i ∈ s, g i) j else 0

Tactic:
split_ifs with hj

Goal state after:
case pos
ι : Type u_1
κ : Type u_2
R : Type u_5
inst✝ : CommSemiring R
s : Finset ι
f : ι → Set κ
g : ι → κ → R
j : κ
hj : j ∈ ⋂ x ∈ s, f x
⊢ ∏ i ∈ s, (f i).indicator (g i) j = (∏ i ∈ s, g i) j

case neg
ι : Type u_1
κ : Type u_2
R : Type u_5
inst✝ : CommSemiring R
s : Finset ι
f : ι → Set κ
g : ι → κ → R
j : κ
hj : j ∉ ⋂ x ∈ s, f x
⊢ ∏ i ∈ s, (f i).indicator (g i) j = 0
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 ι
ha : ∀ 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:
ihs

Goal state after:
ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : LinearOrder ι
f g : ι → R
a : ι
s : Finset ι
ha : ∀ x ∈ s, x < a
ihs : ∏ 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: case inr
K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : V
s q : Submodule K V
hpq : s < q
hqp : q < K ∙ x ⊔ s
c : K
z : V
hz : z ∈ s
hyq : c • x + z ∈ q
hyp : c • x + z ∉ s
hc : c ≠ 0
⊢ K ∙ x ⊔ s ≤ q

Tactic:
have : x ∈ q := by
      rwa [q.add_mem_iff_left (hpq.le hz), q.smul_mem_iff hc] at hyq

Goal state after:
case inr
K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : V
s q : Submodule K V
hpq : s < q
hqp : q < K ∙ x ⊔ s
c : K
z : V
hz : z ∈ s
hyq : c • x + z ∈ q
hyp : c • x + z ∉ s
hc : c ≠ 0
this : x ∈ q
⊢ K ∙ x ⊔ s ≤ q
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✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : f.range = ⊤
p : Submodule R M
⊢ map f p = ⊤ ↔ p ⊔ f.ker = ⊤

Tactic:
simp_rw [← top_le_iff, ← hf, range_eq_map, LinearMap.map_le_map_iff]

Goal state after:
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: ι : Type u_1
F : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
G : Type u_6
H : Type u_7
inst✝¹ : AddZeroClass M
inst✝ : AddZeroClass N
f✝ : M → N
g₁ g₂ : ι →₀ M
f : ι ↪ F
v w : ι →₀ M
b : F
⊢ (embDomain f (v + w)) b = (embDomain f v + embDomain f w) b

Tactic:
by_cases h : b ∈ Set.range f

Goal state after:
case pos
ι : Type u_1
F : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
G : Type u_6
H : Type u_7
inst✝¹ : AddZeroClass M
inst✝ : AddZeroClass N
f✝ : M → N
g₁ g₂ : ι →₀ M
f : ι ↪ F
v w : ι →₀ M
b : F
h : b ∈ Set.range ⇑f
⊢ (embDomain f (v + w)) b = (embDomain f v + embDomain f w) b

case neg
ι : Type u_1
F : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
G : Type u_6
H : Type u_7
inst✝¹ : AddZeroClass M
inst✝ : AddZeroClass N
f✝ : M → N
g₁ g₂ : ι →₀ M
f : ι ↪ F
v w : ι →₀ M
b : F
h : b ∉ Set.range ⇑f
⊢ (embDomain f (v + w)) b = (embDomain f v + embDomain f w) b
Module: Mathlib.Data.Finsupp.Single

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
f : α → M
⊢ {a}.indicator f = ⇑(single a (f a))

Tactic:
rw [Set.indicator_singleton, single_eq_pi_single]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
a : α
m : M
b : β
⊢ (embDomain f (single a m)) b = (single (f a) m) b

Tactic:
by_cases h : b ∈ Set.range f

Goal state after:
case pos
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
a : α
m : M
b : β
h : b ∈ Set.range ⇑f
⊢ (embDomain f (single a m)) b = (single (f a) m) b

case neg
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
a : α
m : M
b : β
h : b ∉ Set.range ⇑f
⊢ (embDomain f (single a m)) b = (single (f a) m) b
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: ι : Type u_1
G : Type u_6
inst✝ : AddGroup G
f : ι →₀ G
a : ι
b : G
⊢ erase a f + single a b = f - single a (f a) + single a b

Tactic:
erase_eq_sub_single

Goal state after:
ι : Type u_1
G : Type u_6
inst✝ : AddGroup G
f : ι →₀ G
a : ι
b : G
⊢ f - single a (f a) + single a b = f - single a (f a) + single a b