mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case pos
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j.succ < n + 2
hij : i < j.succ
⊢ ((↑v).insertIdx j.succ a).eraseIdx ↑⟨i, ⋯⟩ =
    (↑(match v with
          | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)).insertIdx
      (↑(⟨j.succ, hj⟩.pred ⋯)) a

Tactic:
← List.insertIdx_eraseIdx_of_ge

Goal state after:
case pos
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j.succ < n + 2
hij : i < j.succ
⊢ ((↑v).eraseIdx ↑⟨i, ⋯⟩).insertIdx j a =
    (↑(match v with
          | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)).insertIdx
      (↑(⟨j.succ, hj⟩.pred ⋯)) a

case pos.a
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j.succ < n + 2
hij : i < j.succ
⊢ ↑⟨i, ⋯⟩ < (↑v).length

case pos.a
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j.succ < n + 2
hij : i < j.succ
⊢ ↑⟨i, ⋯⟩ ≤ j
Module: Mathlib.Order.SuccPred.CompleteLinearOrder

Goal state before:
pp: α : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : SuccOrder α
x : α
H : BddAbove (range fun a ↦ succ ↑a)
⊢ ⨆ a, succ ↑a ≤ x

Tactic:
ciSup_le_iff' H

Goal state after:
α : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : SuccOrder α
x : α
H : BddAbove (range fun a ↦ succ ↑a)
⊢ ∀ (i : ↑(Iio x)), succ ↑i ≤ x
Module: Mathlib.Order.UpperLower.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
s : Set α
inst✝ : WellFoundedLT α
h : IsLowerSet s
⊢ s = univ ∨ ∃ a, s = Iio a

Tactic:
by
  simp_rw [← @compl_inj_iff _ s]
  simpa using h.compl.eq_empty_or_Ici

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
inst✝ : PartialOrder α
f : α ≤i β
⊢ IsMin (f a) ↔ IsMin a

Tactic:
by
  refine ⟨StrictMono.isMin_of_apply f.strictMono, fun h b hb ↦ ?_⟩
  obtain ⟨x, rfl⟩ := f.mem_range_of_le hb
  rw [f.le_iff_le] at hb ⊢
  exact h hb

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: case pos
α : Type u_4
β : Type u_5
a : Part α
inst✝ : Decidable a.Dom
b : β
f : α → β
h : a.Dom
⊢ a.toOption.elim b f = f (a.get h)

Tactic:
rw [h.toOption]
    rfl

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: case inr
α : Type u_1
x y z : Part α
hx✝¹ : x ≤ z
hy✝ : y ≤ z
b : α
h₀ : b ∈ x
b' : α
h₁ : b' ∈ y
hx✝ : b ∈ z
hy : b' ∈ z
hx : b = b'
⊢ b' ∈ x

Tactic:
subst hx

Goal state after:
case inr
α : Type u_1
x y z : Part α
hx✝ : x ≤ z
hy✝ : y ≤ z
b : α
h₀ : b ∈ x
hx : b ∈ z
h₁ : b ∈ y
hy : b ∈ z
⊢ b ∈ x
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case base_isLeast
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
⊢ IsLeast {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)} x

pp: case image_self_subset_self
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
⊢ f '' {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)} ⊆ {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}

pp: case cSup_mem
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
⊢ ∀ (c : NonemptyChain α), ↑c ⊆ {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)} → cSup c ∈ {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}

Tactic:
· constructor
      · constructor
        · exact (bot_isAdmissible le_map).base_isLeast.1
        · exact Or.inl ((bot_isAdmissible le_map).base_isLeast.2 hy.mem_bot)
      · exact fun y h ↦ (bot_isAdmissible le_map).base_isLeast.2 h.1

Goal state after:
case image_self_subset_self
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
⊢ f '' {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)} ⊆ {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}

case cSup_mem
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
⊢ ∀ (c : NonemptyChain α), ↑c ⊆ {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)} → cSup c ∈ {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case right
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
⊢ ωSup c ∈ lowerBounds (upperBounds (Set.range ⇑c))

Tactic:
· simp only [lowerBounds, upperBounds, Set.mem_range, forall_exists_index,
      forall_apply_eq_imp_iff, Set.mem_ofPred_eq]
    exact fun ⦃a⦄ a_1 ↦ ωSup_le c a a_1

Goal state after:
Module: Mathlib.Order.CompleteLattice.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
c₁ c₂ : Set α
hc₁ : ChainClosure r c₁
hc₂ : ChainClosure r c₂
h : c₁ ⊆ c₂
⊢ c₂ = c₁ ∨ SuccChain r c₁ ⊆ c₂

Tactic:
by
  induction hc₂ generalizing c₁ hc₁ with
  | succ _ ih =>
    refine ((chainClosure_succ_total_aux hc₁) fun c₁ => ih).imp h.antisymm' fun h₁ => ?_
    obtain rfl | h₂ := ih hc₁ h₁
    · exact Subset.rfl
    · exact h₂.trans subset_succChain
  | union _ ih =>
    apply Or.imp_left h.antisymm'
    apply by_contradiction
    simp only [sUnion_subset_iff, not_or, not_forall, exists_prop, and_imp, forall_exists_index]
    intro c₃ hc₃ h₁ h₂
    obtain h | h := chainClosure_succ_total_aux hc₁ fun c₄ => ih _ hc₃
    · exact h₁ (subset_succChain.trans h)
    obtain h' | h' := ih c₃ hc₃ hc₁ h
    · exact h₁ h'.subset
    · exact h₂ (h'.trans <| subset_sUnion_of_mem hc₃)

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

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{v}
hω : ¬IsSuccPrelimit (⨆ i, f i)
⊢ ∃ i, f i = ⨆ i, f i

Tactic:
exact exists_eq_ciSup_of_not_isSuccPrelimit hω

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

Goal state before:
pp: a : Cardinal.{u}
⊢ lift.{v, u} a ≤ 1 ↔ a ≤ 1

Tactic:
by
  simpa using lift_le_nat_iff (n := 1)

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

Goal state before:
pp: x : Cardinal.{u_1}
n : ℕ
⊢ x.toENatAux = ↑n ↔ x = ↑n

Tactic:
by
  simp only [le_antisymm_iff, toENatAux_le_nat, ← toENatAux_gc _, ofENat_nat]

Goal state after:
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
a : R
s : S
inst✝⁴ : Monoid S
inst✝³ : SMul R M
inst✝² : SMul R S
inst✝¹ : MulAction S M
inst✝ : IsScalarTower R S M
h : a • s = 1
⊢ IsSMulRegular M (a • s)

Tactic:
by
      rw [h]
      exact one M

Goal state after:
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : MonoidWithZero R
inst✝¹ : Zero M
inst✝ : MulActionWithZero R M
h : IsSMulRegular M 0
a b : M
⊢ 0 • a = 0 • b

Tactic:
rw [MulActionWithZero.zero_smul]

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : MonoidWithZero R
inst✝¹ : Zero M
inst✝ : MulActionWithZero R M
h : IsSMulRegular M 0
a b : M
⊢ 0 = 0 • b
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : MonoidWithZero R
inst✝¹ : Zero M
inst✝ : MulActionWithZero R M
h : IsSMulRegular M 0
a b : M
⊢ 0 = 0 • b

Tactic:
rw [MulActionWithZero.zero_smul]

Goal state after:
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: R : Type u_1
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G R
g : G
x y : R
h : (fun x ↦ g • x) x = (fun x ↦ g • x) y
⊢ x = y

Tactic:
convert congr_arg (g⁻¹ • ·) h

Goal state after:
case e'_2
R : Type u_1
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G R
g : G
x y : R
h : (fun x ↦ g • x) x = (fun x ↦ g • x) y
⊢ x = g⁻¹ • (fun x ↦ g • x) x

case e'_3
R : Type u_1
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G R
g : G
x y : R
h : (fun x ↦ g • x) x = (fun x ↦ g • x) y
⊢ y = g⁻¹ • (fun x ↦ g • x) y
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α β : Type u
a : Cardinal.{u}
⊢ Small.{u, u + 1} ↑(Iic a)

Tactic:
by
  rw [← mk_out a]
  apply @small_of_surjective (Set a.out) (Iic #a.out) _ fun x => ⟨#x, mk_set_le x⟩
  rintro ⟨x, hx⟩
  simpa using le_mk_iff_exists_set.1 hx

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

Goal state before:
pp: S : Set ℕ
h' : #↑S < #ℕ
h : lift.{u_1, 0} #↑S < ℵ₀
⊢ S.Finite

Tactic:
contrapose! h'

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

Goal state before:
pp: ⊢ (sum fun n ↦ 0 ^ n) = 1

Tactic:
rw [← mk_eq_zero (α := PEmpty), ← mk_list_eq_sum_pow, mk_eq_one]

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

Goal state before:
pp: R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Module R A
h₁ : ∀ (r : R) (x y : A), r • x * y = r • (x * y)
h₂ : ∀ (r : R) (x y : A), x * r • y = r • (x * y)
r : R
x : A
⊢ r • 1 * x = r • x

Tactic:
h₁,

Goal state after:
R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Module R A
h₁ : ∀ (r : R) (x y : A), r • x * y = r • (x * y)
h₂ : ∀ (r : R) (x y : A), x * r • y = r • (x * y)
r : R
x : A
⊢ r • (1 * x) = r • x
Module: Mathlib.Algebra.Algebra.Defs

Goal state before:
pp: R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Module R A
h₁ : ∀ (r : R) (x y : A), r • x * y = r • (x * y)
h₂ : ∀ (r : R) (x y : A), x * r • y = r • (x * y)
r : R
x : A
⊢ r • 1 * x = r • x

Tactic:
by rw [h₁, one_mul]

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

Goal state before:
pp: R : Type u_1
S : Type u_5
M : Type u_8
M₃ : Type u_11
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module S M₃
σ : R →+* S
F : Type u_14
inst✝¹ : FunLike F M M₃
inst✝ : SemilinearMapClass F σ M M₃
f g : F
h : ↑f = ↑g
m : M
⊢ f m = g m

Tactic:
exact DFunLike.congr_fun h m

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

Goal state before:
pp: 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
inst✝ : RingHomSurjective σ₂₁
p : Submodule R₂ M₂
q : Submodule R M
f : M₂ →ₛₗ[σ₂₁] M
h : ∀ x ∈ p, f x ∈ q
p' : Submodule R₂ ↥p
⊢ comap q.subtype (map (f.domRestrict p) p') = comap q.subtype (map f (map p.subtype p'))

Tactic:
map_domRestrict

Goal state after:
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
inst✝ : RingHomSurjective σ₂₁
p : Submodule R₂ M₂
q : Submodule R M
f : M₂ →ₛₗ[σ₂₁] M
h : ∀ x ∈ p, f x ∈ q
p' : Submodule R₂ ↥p
⊢ comap q.subtype (map f (map p.subtype p')) = comap q.subtype (map f (map p.subtype p'))
Module: Mathlib.Algebra.Ring.Submonoid.Basic

Goal state before:
pp: M : Type u_1
R : Type u_2
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike M R
inst✝ : MulMemClass M R
S : M
a b : R
ha : a ∈ closure ↑S
hb : b ∈ S
⊢ a * b ∈ closure ↑S

Tactic:
induction ha using closure_induction with
  | mem r hr => exact mem_closure.mpr fun y hy => hy (mul_mem hr hb)
  | zero => simp only [zero_mul, zero_mem _]
  | add r s _ _ hr hs => simpa only [add_mul] using add_mem hr hs

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

Goal state before:
pp: R : Type u_6
S : Type u_7
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : IsDomain (R × S)
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
this : 0 = 0 ∧ 1 = 0 ∨ 1 = 0 ∧ 0 = 0
⊢ False

Tactic:
rcases this with (⟨_, h⟩ | ⟨h, _⟩)

Goal state after:
case inl
R : Type u_6
S : Type u_7
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : IsDomain (R × S)
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
left✝ : 0 = 0
h : 1 = 0
⊢ False

case inr
R : Type u_6
S : Type u_7
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : IsDomain (R × S)
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
h : 1 = 0
right✝ : 0 = 0
⊢ False
Module: Mathlib.Algebra.Algebra.Basic

Goal state before:
pp: R✝ : Type u_1
inst✝¹¹ : CommSemiring R✝
A✝ : Type u_2
inst✝¹⁰ : Semiring A✝
inst✝⁹ : Algebra R✝ A✝
M : Type u_3
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module A✝ M
inst✝⁶ : Module R✝ M
inst✝⁵ : IsScalarTower R✝ A✝ M
R : Type u_4
S : Type u_5
A : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Algebra S A
r : R
s : S
a : A
⊢ s • ((algebraMap R A) r * a) = s • r • a

Tactic:
← Algebra.smul_def

Goal state after:
R✝ : Type u_1
inst✝¹¹ : CommSemiring R✝
A✝ : Type u_2
inst✝¹⁰ : Semiring A✝
inst✝⁹ : Algebra R✝ A✝
M : Type u_3
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module A✝ M
inst✝⁶ : Module R✝ M
inst✝⁵ : IsScalarTower R✝ A✝ M
R : Type u_4
S : Type u_5
A : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Algebra S A
r : R
s : S
a : A
⊢ s • r • a = s • r • a
Module: Mathlib.Algebra.Algebra.Hom

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
M : Submonoid R
B : Type w
inst✝¹ : Semiring B
inst✝ : Algebra R B
f : A →ₐ[R] B
⊢ algebraMapSubmonoid A M ≤ Submonoid.comap f.toRingHom (algebraMapSubmonoid B M)

Tactic:
rw [← algebraMapSubmonoid_map_eq M f]
  exact Submonoid.le_comap_map (Algebra.algebraMapSubmonoid A M)

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀ : Type u_4
S : Type u_5
F : Type u_6
inst✝³ : MonoidWithZero M₀
inst✝² : MonoidWithZero S
inst✝¹ : EquivLike F M₀ S
inst✝ : MulEquivClass F M₀ S
h✝ : F
h : M₀ ≃* S := ↑h✝
x✝ : S
⊢ x✝ ∈ Submonoid.comap h.symm M₀⁰ ↔ x✝ ∈ S⁰

Tactic:
Submonoid.mem_comap,

Goal state after:
M₀ : Type u_4
S : Type u_5
F : Type u_6
inst✝³ : MonoidWithZero M₀
inst✝² : MonoidWithZero S
inst✝¹ : EquivLike F M₀ S
inst✝ : MulEquivClass F M₀ S
h✝ : F
h : M₀ ≃* S := ↑h✝
x✝ : S
⊢ h.symm x✝ ∈ M₀⁰ ↔ x✝ ∈ S⁰
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case refine_2.inl
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
x y : M
hx : Prime x
hy : IsUnit y
⊢ Prime (x * y)

Tactic:
exact (associated_mul_unit_left x y hy).symm.prime hx

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀ : Type u_4
S : Type u_5
F : Type u_6
inst✝³ : MonoidWithZero M₀
inst✝² : MonoidWithZero S
inst✝¹ : EquivLike F M₀ S
inst✝ : MulEquivClass F M₀ S
h : F
⊢ Submonoid.map h M₀⁰ = S⁰

Tactic:
by
  let h : M₀ ≃* S := h
  change Submonoid.map h _ = _
  ext
  simp_rw [Submonoid.map_equiv_eq_comap_symm, Submonoid.mem_comap, mem_nonZeroDivisors_iff,
    ← h.symm.forall_congr_right, h.symm.toEquiv_eq_coe, h.symm.coe_toEquiv, ← map_mul,
    map_eq_zero_iff _ h.symm.injective]

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

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p p' : Submodule R M
⊢ map p.subtype ⊤ ≤ p' ↔ p ≤ p'

Tactic:
rw [map_subtype_top]

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
K : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
V₂ : Type u_9
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
p : Submodule R M
τ₁₂ : R →+* R₂
p' : Submodule R ↥p
⊢ Injective ⇑p.subtype

Tactic:
by exact Subtype.val_injective

Goal state after:
Module: Mathlib.Algebra.Order.Group.Action

Goal state before:
pp: G : Type u_4
inst✝³ : Monoid G
α : Type u_5
inst✝² : Preorder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : a ≤ g • a
n : ℕ
⊢ a ≤ g ^ n • a

Tactic:
induction n with
  | zero => rw [pow_zero, one_smul]
  | succ n hn =>
    rw [pow_succ', mul_smul]
    exact h.trans (smul_mono_right g hn)

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
⊢ f.rangeRestrict.range = ⊤

Tactic:
simp [f.range_codRestrict _]

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

Goal state before:
pp: case smul
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x : M
r₁ : R
y : M
hy : y ∈ closure (univ • s)
⊢ r₁ • y ∈ closure (univ • s)

Tactic:
induction hy using closure_induction with
      | mem _ h =>
        obtain ⟨r₂, -, x, hx, rfl⟩ := h
        exact subset_closure ⟨r₁ * r₂, trivial, x, hx, mul_smul ..⟩
      | zero => simp only [smul_zero, zero_mem]
      | add _ _ _ _ h₁ h₂ => simpa only [smul_add] using add_mem h₁ h₂

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

Goal state before:
pp: case refine_3
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
h : x ∈ R ∙ y
⊢ ∀ (x y_1 : M), x ∈ R ∙ y → y_1 ∈ R ∙ y → (∃ a, a • y = x) → (∃ a, a • y = y_1) → ∃ a, a • y = x + y_1

Tactic:
rintro _ _ - - ⟨a, rfl⟩ ⟨b, rfl⟩
      exact ⟨a + b, by simp [add_smul]⟩

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:
← singleton_subset_iff

Goal state after:
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)
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α✝
α : Type u_4
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
⊢ ∃ s, b = sSup s ∧ ∀ a ∈ s, IsAtom a

Tactic:
refine ⟨{ a | IsAtom a ∧ a ≤ b }, ?_, fun a ha => ha.1⟩

Goal state after:
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α✝
α : Type u_4
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
⊢ b = sSup {a | IsAtom a ∧ a ≤ b}
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inr
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α✝
inst✝⁴ : BoundedOrder α✝
inst✝³ : IsSimpleOrder α✝
α : Type ?u.12
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
b c : α
⊢ ⊤ ≤ b → b ≤ c → ⊤ ≤ c

Tactic:
· rcases eq_bot_or_eq_top b with (rfl | rfl)
      · rcases eq_bot_or_eq_top c with (rfl | rfl) <;> simp
      · simp

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁷ : DecidableEq α✝
inst✝⁶ : PartialOrder α✝
inst✝⁵ : BoundedOrder α✝
inst✝⁴ : IsSimpleOrder α✝
α : Type ?u.16
inst✝³ : DecidableEq α
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
x : α
⊢ (x ⊓ if x = ⊥ then ⊤ else ⊥) ≤ ⊥

Tactic:
rcases eq_bot_or_eq_top x with (rfl | rfl)
      · simp
      · simp

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
s : Set α
⊢ IsAtom sᶜ ↔ ∃ x, s = {x}ᶜ

Tactic:
isAtom_iff

Goal state after:
α : Type u_2
s : Set α
⊢ (∃ x, sᶜ = {x}) ↔ ∃ x, s = {x}ᶜ
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_5
inst✝ : CompleteLattice α
s : Set α
⊢ (∀ ⦃a : α⦄, a ∈ s → Disjoint a (sSup (s \ {a}))) ↔ ∀ (i : { x // x ∈ s }), Disjoint (↑i) (⨆ j, ⨆ (_ : j ≠ i), ↑j)

Tactic:
SetCoe.forall,

Goal state after:
α : Type u_5
inst✝ : CompleteLattice α
s : Set α
⊢ (∀ ⦃a : α⦄, a ∈ s → Disjoint a (sSup (s \ {a}))) ↔ ∀ (x : α) (h : x ∈ s), Disjoint x (⨆ j, ⨆ (_ : j ≠ ⟨x, h⟩), ↑j)
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
ι : Sort u_5
ι' : Sort u_6
t : ι → α
f : ι' → ι
ht : iSupIndep (t ∘ f)
hf : Surjective f
⊢ iSupIndep t

Tactic:
intro i
  obtain ⟨i', rfl⟩ := hf i
  rw [← hf.iSup_comp]
  exact (ht i').mono_right (biSup_mono fun j' hij => mt (congr_arg f) hij)

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
⊢ sSup {a | IsCompactElement a} = ⊤

Tactic:
← sSup_compact_le_eq ⊤

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
⊢ sSup {a | IsCompactElement a} = sSup {c | IsCompactElement c ∧ c ≤ ⊤}
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
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
S : Set M
f g : ↥(span R S) →ₗ[R] N
h : ∀ (s : ↑S), f ⟨↑s, ⋯⟩ = g ⟨↑s, ⋯⟩
this : ∀ (x : M) (hx : x ∈ span R S), f ⟨x, hx⟩ = g ⟨x, hx⟩
x : M
hx : x ∈ span R S
⊢ f ⟨x, hx⟩ = g ⟨x, hx⟩

Tactic:
exact this x hx

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
η : Type u_3
s : η → Set α
hs : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ (i : η), sSupIndep (s i)
⊢ sSupIndep (⋃ i, s i)

Tactic:
by_cases hη : Nonempty η

Goal state after:
case pos
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
η : Type u_3
s : η → Set α
hs : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ (i : η), sSupIndep (s i)
hη : Nonempty η
⊢ sSupIndep (⋃ i, s i)

case neg
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
η : Type u_3
s : η → Set α
hs : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ (i : η), sSupIndep (s i)
hη : ¬Nonempty η
⊢ sSupIndep (⋃ i, s i)
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case neg.inl
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
h : ¬{c | IsCompactElement c ∧ c ≤ b} ⊆ {⊥}
c : α
hcbot : c ∉ {⊥}
hc : IsCompactElement c
hcb : c ≤ b
hc' : IsAtomic ↑(Iic c)
con : c = ⊥
⊢ c ∈ {⊥}

Tactic:
exact con

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : Zero M
f g : α →₀ M
x✝ : f.support = g.support ∧ ∀ x ∈ f.support, f x = g x
h₁ : f.support = g.support
h₂ : ∀ x ∈ f.support, f x = g x
a : α
h : a ∉ f.support
hf : f a = 0
⊢ g a = 0

Tactic:
h₁,

Goal state after:
α : Type u_1
M : Type u_4
inst✝ : Zero M
f g : α →₀ M
x✝ : f.support = g.support ∧ ∀ x ∈ f.support, f x = g x
h₁ : f.support = g.support
h₂ : ∀ x ∈ f.support, f x = g x
a : α
h : a ∉ g.support
hf : f a = 0
⊢ g a = 0
Module: Mathlib.Data.Finsupp.Defs

Goal state before:
pp: α : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
he : Injective e
⊢ Injective (mapRange e he₀)

Tactic:
by
  intro a b h
  rw [Finsupp.ext_iff] at h ⊢
  simpa only [mapRange_apply, he.eq_iff] using h

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
a : ι
b : M
f : ι →₀ M
ha : a ∉ f.support
hb : b ≠ 0
⊢ (f + single a b).support = cons a f.support ha

Tactic:
have H := support_single a hb
  rw [support_add_eq, H, union_comm, cons_eq_insert, insert_eq]
  rwa [H, disjoint_singleton_right]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Indicator

Goal state before:
pp: α : Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : LinearOrder M
s : Set α
f : α → M
⊢ s.indicator f ≤ {a | 0 ≤ f a}.indicator f

Tactic:
by
  intro a
  classical
  simp_rw [indicator_apply]
  split_ifs
  exacts [le_rfl, (not_le.1 ‹_›).le, ‹_›, le_rfl]

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
f : α →₀ M
⊢ (f.prod fun x x_1 ↦ 1) = 1

Tactic:
by simp [prod]

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
inst✝ : DecidableEq α
f : α →₀ M
a : α
b : α → M → N
⊢ (∏ a_1 ∈ f.support, if a = a_1 then b a_1 (f a_1) else 1) = if a ∈ f.support then b a (f a) else 1

Tactic:
rw [f.support.prod_ite_eq]

Goal state after: