mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Logic.Small.Basic

Goal state before:
pp: case pos
α : Type v
β : Type w
γ : Type v'
inst✝ : Small.{u, v} α
f : α → γ
g : β → γ
hg : Function.Injective g
h : ∀ (b : β), ∃ a, f a = g b
hβ : Nonempty β
b : β
⊢ ∃ a, (Function.invFun g ∘ f) a = b

Tactic:
obtain ⟨a, ha⟩ := h b

Goal state after:
case pos
α : Type v
β : Type w
γ : Type v'
inst✝ : Small.{u, v} α
f : α → γ
g : β → γ
hg : Function.Injective g
h : ∀ (b : β), ∃ a, f a = g b
hβ : Nonempty β
b : β
a : α
ha : f a = g b
⊢ ∃ a, (Function.invFun g ∘ f) a = b
Module: Mathlib.Data.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
π : ι → Sort u_2
f g : (i : ι) → π i
inst✝ : DecidableEq ι
i : ι
⊢ {i}.piecewise f g = update g i (f i)

Tactic:
rw [← insert_empty_eq, piecewise_insert, piecewise_empty]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
s : Finset ι
p : ι → Prop
inst✝ : DecidablePred p
h✝ : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j
a : M
h : ∃ i ∈ s, p i
⊢ (∏ i ∈ s, if p i then a else 1) = a

pp: case neg
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
s : Finset ι
p : ι → Prop
inst✝ : DecidablePred p
h✝ : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j
a : M
h : ¬∃ i ∈ s, p i
⊢ (∏ i ∈ s, if p i then a else 1) = 1

Tactic:
· obtain ⟨i, hi, hpi⟩ := h
    rw [prod_eq_single_of_mem _ hi, if_pos hpi]
    exact fun j hj hji ↦ if_neg fun hpj ↦ hji <| h _ hj _ hi hpj hpi

Goal state after:
case neg
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
s : Finset ι
p : ι → Prop
inst✝ : DecidablePred p
h✝ : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j
a : M
h : ¬∃ i ∈ s, p i
⊢ (∏ i ∈ s, if p i then a else 1) = 1
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
l : List α
e : (a :: l).length = n.succ
i : ℕ
h : i < n
⊢ (tail ⟨a :: l, e⟩).get ⟨i, h⟩ = get ⟨a :: l, e⟩ ⟨i, h⟩.succ

Tactic:
simp [get_eq_get_toList]; rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_6
f : β → α → β
b : β
v : Vector α 1
⊢ scanl f b (v.head ::ᵥ v.tail) = b ::ᵥ f b (v.head ::ᵥ v.tail).head ::ᵥ nil

Tactic:
simp only [scanl_cons, scanl_nil, head_cons, singleton_tail]

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

Goal state before:
pp: α : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
β : Type u_6
γ : Type u_7
a✝ a : α
i : Fin (n + 1)
v : Vector α n
⊢ ((↑v).insertIdx (↑i) a).length = n + 1

Tactic:
rw [List.length_insertIdx, v.2]
    split <;> lia

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

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{v}
a : ι
⊢ Nonempty (Quotient.out (f a) ≃ Quotient.out ((fun i ↦ lift.{w, v} (f i)) a))

Tactic:
rw [← lift_mk_eq.{_, _, v}, mk_out, mk_out, lift_lift]

Goal state after:
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_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_cases h : o.Dom <;> simp [h, toOption]

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case inr
α : Type u_2
c : Chain (Part α)
a b : α
i : ℕ
ha : a ∈ c i
j : ℕ
hb : b ∈ c j
hji : j ≤ i
⊢ a = b

Tactic:
have := c.monotone hji _ hb; apply Eq.symm; apply mem_unique this ha

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case a.zero
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
⊢ (iterateChain (↑f) x h) 0 ≤ ωSup ((iterateChain (↑f) x h).map ↑f)

Tactic:
apply le_trans h
      change ((iterateChain f x h).map f) 0 ≤ ωSup ((iterateChain f x h).map (f : α →o α))
      apply le_ωSup

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

Goal state before:
pp: c : Cardinal.{u}
⊢ lift.{v, u} c = ℵ₀ ↔ c = ℵ₀

Tactic:
simp [eqComm]

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

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

Tactic:
simp [eqComm]

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

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

Tactic:
simp [eqComm]

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

Goal state before:
pp: d : Cardinal.{u}
hd : d < ℵ₀
c : ℕ
⊢ toNat (↑c + d) = toNat ↑c + toNat d

Tactic:
lift d to ℕ using hd

Goal state after:
c d : ℕ
⊢ toNat (↑c + ↑d) = toNat ↑c + toNat ↑d
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: a : Cardinal.{u_1}
⊢ ↑(toENat a) = a ↔ a ≤ ℵ₀

Tactic:
by
  rw [eq_comm, ← enat_gc.exists_eq_l]
  simpa only [mem_range, eq_comm] using! Set.ext_iff.1 range_ofENat a

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

Goal state before:
pp: c : Cardinal.{u}
n : ℕ
⊢ ↑n ≤ toENat c ↔ ↑n ≤ c

Tactic:
← toENat_nat n,

Goal state after:
c : Cardinal.{u}
n : ℕ
⊢ toENat ↑n ≤ toENat c ↔ ↑n ≤ c
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{v}
⊢ sum f ≤ lift.{v, u} #ι * ⨆ i, lift.{u, v} (f i)

Tactic:
rw [← (sum f).lift_id, lift_sum, ← lift_umax.{u, v}, ← (⨆ i, lift (f i)).lift_id,
    lift_umax.{max v u, u}, ← sum_const]

Goal state after:
ι : Type u
f : ι → Cardinal.{v}
⊢ (sum fun i ↦ lift.{max u v, v} (f i)) ≤ sum fun x ↦ ⨆ i, lift.{u, v} (f i)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
β : Type v
⊢ #↑(range Sum.inl) = lift.{v, u} #α

Tactic:
by
  rw [← lift_id'.{u, v} #_, (Equiv.Set.rangeInl α β).lift_cardinal_eq, lift_umax.{u, v}]

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

Goal state before:
pp: case fst
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝⁶ : SMul M α
inst✝⁵ : SMul M β
inst✝⁴ : SMul N α
inst✝³ : SMul N β
a : M
x : α × β
inst✝² : SMul M N
inst✝¹ : IsScalarTower M N α
inst✝ : IsScalarTower M N β
x✝² : M
x✝¹ : N
x✝ : α × β
⊢ ((x✝² • x✝¹) • x✝).1 = (x✝² • x✝¹ • x✝).1

Tactic:
exact smul_assoc ..

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

Goal state before:
pp: case snd
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝⁶ : SMul M α
inst✝⁵ : SMul M β
inst✝⁴ : SMul N α
inst✝³ : SMul N β
a : M
x : α × β
inst✝² : SMul M N
inst✝¹ : IsScalarTower M N α
inst✝ : IsScalarTower M N β
x✝² : M
x✝¹ : N
x✝ : α × β
⊢ ((x✝² • x✝¹) • x✝).2 = (x✝² • x✝¹ • x✝).2

Tactic:
exact smul_assoc ..

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

Goal state before:
pp: case e_3
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
⊢ compHom α (MonoidHom.inl M N) = hM

Tactic:
ext m a

Goal state after:
case e_3
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
m : M
a : α
⊢ SMul.smul m a = SMul.smul m a
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: case e_4.e_2.e_4.e_4.e_4
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
x✝ : MulAction N α
⊢ compHom α (MonoidHom.inl M N) = hM

Tactic:
ext m a

Goal state after:
case e_4.e_2.e_4.e_4.e_4
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
x✝ : MulAction N α
m : M
a : α
⊢ SMul.smul m a = SMul.smul m a
Module: Mathlib.Algebra.GroupWithZero.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → MulZeroClass (α i)
inst✝ : DecidableEq ι
i : ι
f : (i : ι) → α i
⊢ ∀ (a : (i : ι) → α i), 0 * a = 0

Tactic:
by intros; ext; exact zero_mul _

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
S : Type u_5
S₃ : Type u_6
T : Type u_7
M : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module S M₂
σ : R →+* S
σ' : S →+* R
inst✝ : RingHomInvPair σ σ'
f : M →ₛₗ[σ] M₂
g : M₂ → M
h₁ : ∀ (x : M), g (f x) = x
h₂ : ∀ (x : M₂), f (g x) = x
x y : M₂
⊢ g (x + y) = g x + g y

Tactic:
by rw [← h₁ (g (x + y)), ← h₁ (g x + g y)]; simp [h₂]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M' : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
φ : M → N
ψ : N → P
χ : M → P
X : Type u_5
inst✝⁵ : SMul M X
inst✝⁴ : SMul M' X
Y : Type u_6
inst✝³ : SMul N Y
inst✝² : SMul M' Y
Z : Type u_7
inst✝¹ : SMul P Z
φ' : N → M
Y₁ : Type u_8
inst✝ : SMul M Y₁
f : X →ₑ[id] Y₁
g : Y₁ → X
h₁ : Function.LeftInverse g ⇑f
h₂ : Function.RightInverse g ⇑f
m : M
x : Y₁
⊢ g (f (m • g x)) = m • g x

Tactic:
rw [h₁]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M' : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
φ : M → N
ψ : N → P
χ : M → P
X : Type u_5
inst✝⁵ : SMul M X
inst✝⁴ : SMul M' X
Y : Type u_6
inst✝³ : SMul N Y
inst✝² : SMul M' Y
Z : Type u_7
inst✝¹ : SMul P Z
φ' : N → M
Y₁ : Type u_8
inst✝ : SMul M Y₁
f : X →ₑ[φ] Y
g : Y → X
k : Function.RightInverse φ' φ
h₁ : Function.LeftInverse g ⇑f
h₂ : Function.RightInverse g ⇑f
m : N
x : Y
⊢ g (f (φ' m • g x)) = φ' m • g x

Tactic:
rw [h₁]

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

Goal state before:
pp: I : Type u
f : I → Type v
i : I
inst✝ : (i : I) → Distrib (f i)
⊢ ∀ (a b c : (i : I) → f i), a * (b + c) = a * b + a * c

Tactic:
by intros; ext; exact mul_add _ _ _

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Prod

Goal state before:
pp: case e_3
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 α
⊢ compHom α (MonoidHom.inl M N) = fst✝

Tactic:
ext m a

Goal state after:
case e_3
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 α
m : M
a : α
⊢ SMul.smul m a = SMul.smul m a
Module: Mathlib.Algebra.GroupWithZero.Action.Prod

Goal state before:
pp: case e_4.e_2.e_4.e_4.e_4.e_5
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 α
i : DistribMulAction N α
⊢ compHom α (MonoidHom.inl M N) = fst✝

Tactic:
ext m a

Goal state after:
case e_4.e_2.e_4.e_4.e_4.e_5
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 α
i : DistribMulAction N α
m : M
a : α
⊢ SMul.smul m a = SMul.smul m a
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₂
p : Submodule R M
q : Submodule R₂ M₂
inst✝ : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Surjective ⇑f
h : comap f q ≤ p ∧ ¬p ≤ comap f q
⊢ q ≤ map f p ∧ ¬p ≤ comap f q

Tactic:
exact h.imp_left (le_map_of_comap_le_of_surjective hf)

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

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
ϕ : R →+* S
hϕ : Injective ⇑ϕ
hR : CharZero R
⊢ Injective Nat.cast

Tactic:
by intro a b h; rwa [← @Nat.cast_inj R, ← hϕ.eq_iff, map_natCast ϕ, map_natCast ϕ]

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 = 0
⊢ n = 0 ∨ a = b

Tactic:
← mul_sub,

Goal state after:
R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
n : ℕ
a b : R
h : ↑n * (a - b) = 0
⊢ n = 0 ∨ a = b
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocSemiring R
s : Set R
x : R
⊢ x ∈ closure ↑(AddSubmonoid.closure s) ↔ x ∈ closure s

Tactic:
refine ⟨fun hx => ?_, fun hx => closure_mono AddSubmonoid.subset_closure hx⟩

Goal state after:
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
s : Set R
x : R
hx : x ∈ closure ↑(AddSubmonoid.closure s)
⊢ x ∈ closure s
Module: Mathlib.RingTheory.NonUnitalSubring.Basic

Goal state before:
pp: case mem
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x x✝ : R
hx : x✝ ∈ ↑(Subsemigroup.closure s)
⊢ x✝ ∈ closure s

Tactic:
induction hx using Subsemigroup.closure_induction with
      | mem _ h => exact subset_closure h
      | mul _ _ _ _ h₁ h₂ => exact mul_mem h₁ h₂

Goal state after:
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonAssocSemiring R
s : Set R
x : R
⊢ x ∈ closure ↑(AddSubmonoid.closure s) ↔ x ∈ closure s

Tactic:
refine ⟨fun hx => ?_, fun hx => closure_mono AddSubmonoid.subset_closure hx⟩

Goal state after:
R : Type u
inst✝ : NonAssocSemiring R
s : Set R
x : R
hx : x ∈ closure ↑(AddSubmonoid.closure s)
⊢ x ∈ closure s
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 : R
a : A
m : M
⊢ a • (algebraMap R A) r • m = a • r • m

Tactic:
←
      algebra_compatible_smul

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 : R
a : A
m : M
⊢ a • r • m = a • r • m
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonAssocRing R
ι : Sort u_1
hι : Nonempty ι
S : ι → Subring R
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : R
⊢ x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i

Tactic:
refine ⟨?_, fun ⟨i, hi⟩ ↦ le_iSup S i hi⟩
  let U : Subring R :=
    Subring.mk' (⋃ i, (S i : Set R)) (⨆ i, (S i).toSubmonoid) (⨆ i, (S i).toAddSubgroup)
      (Submonoid.coe_iSup_of_directed hS) (AddSubgroup.coe_iSup_of_directed hS)
  suffices ⨆ i, S i ≤ U by simpa [U] using @this x
  exact iSup_le fun i x hx ↦ Set.mem_iUnion.2 ⟨i, hx⟩

Goal state after:
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 : p * b = a * (p * x)
⊢ p ∣ a ∨ a ∣ b

Tactic:
rw [mul_left_comm, mul_right_inj' hp.ne_zero] at hc
    exact Or.inr (hc.symm ▸ dvd_mul_right _ _)

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p a : M
n : ℕ
hp : Prime p
x : M
hb : ¬p ^ 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
y : M
hy : a ^ n.succ * (p * x) ^ n = p ^ n.succ * y
⊢ p ^ n * (a ^ n.succ * x ^ n) = p ^ n * (p * y)

Tactic:
rw [← mul_assoc _ p, ← pow_succ, ← hy, mul_pow, ← mul_assoc (a ^ n.succ), mul_comm _ (p ^ n),
      mul_assoc]

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

Goal state before:
pp: case pos
M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : IsLeftCancelMulZero M
a c d : M
a_eq : a = a * c * d
ha0 : a = 0
⊢ a ~ᵤ a * c

pp: case neg
M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : IsLeftCancelMulZero M
a c d : M
a_eq : a = a * c * d
ha0 : ¬a = 0
⊢ a ~ᵤ a * c

Tactic:
· simp_all

Goal state after:
case neg
M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : IsLeftCancelMulZero M
a c d : M
a_eq : a = a * c * d
ha0 : ¬a = 0
⊢ a ~ᵤ a * c
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : M
n : ℕ
⊢ Prime (p ^ n) ↔ Prime p ∧ n = 1

Tactic:
refine ⟨fun hp ↦ ?_, fun ⟨hp, hn⟩ ↦ by simpa [hn]⟩
  suffices n = 1 by simp_all
  grind [not_prime_pow, Nat.zero_eq_one_mod_iff]

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

Goal state before:
pp: case h
M : Type u_1
inst✝ : CommMonoid M
a b : M
hab : ⟦a⟧ * ⟦b⟧ = 1
hba : ⟦b⟧ * ⟦a⟧ = 1
⊢ { val := ⟦a⟧, inv := ⟦b⟧, val_inv := hab, inv_val := hba } = default

Tactic:
exact Units.ext <| Quotient.sound <| associated_one_of_associated_mul_one <| Quotient.exact hab

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

Goal state before:
pp: case mp
M : Type u_1
inst✝ : CommMonoidWithZero M
a b : M
⊢ (∃ x, ¬IsUnit x ∧ a * x ~ᵤ b) → ∃ x, ¬IsUnit x ∧ b = a * x

pp: case mpr
M : Type u_1
inst✝ : CommMonoidWithZero M
a b : M
⊢ (∃ x, ¬IsUnit x ∧ b = a * x) → ∃ x, ¬IsUnit x ∧ a * x ~ᵤ b

Tactic:
· rintro ⟨x, hx, u, rfl⟩
    refine ⟨x * u, ?_, mul_assoc ..⟩
    simpa

Goal state after:
case mpr
M : Type u_1
inst✝ : CommMonoidWithZero M
a b : M
⊢ (∃ x, ¬IsUnit x ∧ b = a * x) → ∃ x, ¬IsUnit x ∧ a * x ~ᵤ b
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.range = ⊤ ↔ Surjective ⇑f

Tactic:
by
  rw [SetLike.ext'_iff, coe_range, top_coe, Set.range_eq_univ]

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

Goal state before:
pp: case succ.inr
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : M
hp : Prime p
n : ℕ
ih : ∀ {q : M}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : M
h : q ∣ p * p ^ n
hno : q ∣ p ^ n
i : ℕ
hi : i ≤ n
hq : q ~ᵤ p ^ i
⊢ ∃ i, i ≤ n + 1 ∧ q ~ᵤ p ^ i

Tactic:
exact ⟨i, hi.trans n.le_succ, hq⟩

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝ : Frame α
f : ι → α
a : α
ha : IsAtom a
h : a ≤ ⨆ i, f i
ha' : ∀ (i : ι), ¬a ≤ f i
i : ι
x : α
hxa : x ≤ a
hxf : x ≤ f i
hx : ¬x = ⊥
⊢ ¬x = a

Tactic:
rintro rfl; exact ha' _ hxf

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝ : PartialOrder α
b : α
a : ↑(Iic b)
⊢ (range ⇑(OrderEmbedding.subtype fun c ↦ c ≤ b)).OrdConnected

Tactic:
simpa only [OrderEmbedding.coe_subtype, Subtype.range_coe_subtype] using! Set.ordConnected_Iic

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inl
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : IsAtomistic α
b : α
hsb : IsLUB ∅ b
hs : ∀ a ∈ ∅, IsAtom a
⊢ b = ⊥ ∨ ∃ a, IsAtom a ∧ a ≤ b

pp: case inr
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : IsAtomistic α
b : α
s : Set α
hsb : IsLUB s b
hs : ∀ a ∈ s, IsAtom a
a : α
ha : a ∈ s
⊢ b = ⊥ ∨ ∃ a, IsAtom a ∧ a ≤ b

Tactic:
· simp_all

Goal state after:
case inr
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : IsAtomistic α
b : α
s : Set α
hsb : IsLUB s b
hs : ∀ a ∈ s, IsAtom a
a : α
ha : a ∈ s
⊢ b = ⊥ ∨ ∃ a, IsAtom a ∧ a ≤ b
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inl
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : IsCoatomistic α
b : α
hsb : IsGLB ∅ b
hs : ∀ a ∈ ∅, IsCoatom a
⊢ b = ⊤ ∨ ∃ a, IsCoatom a ∧ b ≤ a

pp: case inr
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : IsCoatomistic α
b : α
s : Set α
hsb : IsGLB s b
hs : ∀ a ∈ s, IsCoatom a
a : α
ha : a ∈ s
⊢ b = ⊤ ∨ ∃ a, IsCoatom a ∧ b ≤ a

Tactic:
· simp_all

Goal state after:
case inr
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : IsCoatomistic α
b : α
s : Set α
hsb : IsGLB s b
hs : ∀ a ∈ s, IsCoatom a
a : α
ha : a ∈ s
⊢ b = ⊤ ∨ ∃ a, IsCoatom a ∧ b ≤ a
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
s : Set M
⊢ (∃ a, x + a • y ∈ span R s) → ∃ a, ∃ z ∈ span R s, x = a • y + z

Tactic:
rintro ⟨a, h⟩

Goal state after:
case mpr
R : Type u_1
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
s : Set M
a : R
h : x + a • y ∈ span R s
⊢ ∃ a, ∃ z ∈ span R s, x = a • y + z
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_8
A : Type u_9
inst✝⁴ : Semiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
x : A
h : ∀ y ∈ s, Commute x y
⊢ ∀ y ∈ span R s, Commute x y

Tactic:
simp only [Commute.symm_iff (a := x)] at *
  exact .span_left h

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case hsup
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝³ : Lattice α
inst✝² : IsModularLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → Finset ι
f : ι → α
hs : s.SupIndep fun i ↦ (g i).sup f
hg : ∀ i' ∈ s, (g i').SupIndep f
a : Finset ι
ha : a ⊆ s.biUnion g
b : ι
hb✝ : b ∈ s.biUnion g
hab : b ∉ a
i' : ι'
hi' : i' ∈ s
hb : b ∈ g i'
t : Finset ι' := s.erase i'
u : Finset ι := (g i').erase b
⊢ Disjoint (t.sup fun i ↦ (g i).sup f) (u.sup f ⊔ {b}.sup f)

Tactic:
← sup_union,

Goal state after:
case hsup
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝³ : Lattice α
inst✝² : IsModularLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → Finset ι
f : ι → α
hs : s.SupIndep fun i ↦ (g i).sup f
hg : ∀ i' ∈ s, (g i').SupIndep f
a : Finset ι
ha : a ⊆ s.biUnion g
b : ι
hb✝ : b ∈ s.biUnion g
hab : b ∉ a
i' : ι'
hi' : i' ∈ s
hb : b ∈ g i'
t : Finset ι' := s.erase i'
u : Finset ι := (g i').erase b
⊢ Disjoint (t.sup fun i ↦ (g i).sup f) ((u ∪ {b}).sup f)
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
h : ∀ (i : { i // t i ≠ ⊥ }), Disjoint (t ↑i) (⨆ j, ⨆ (_ : j ≠ i), t ↑j)
i : ι
hi : t i ≠ ⊥
j : ι
⊢ ⨆ (_ : t j = ⊥), t j = ⊥

Tactic:
simp only [iSup_eq_bot, imp_self]

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case insert
α : Type u_1
ι : Type u_3
inst✝¹ : CompleteLattice α
inst✝ : IsModularLattice α
f : ι → α
hf : iSupIndep f
j : ι
s₀ : Finset ι
hj : j ∉ s₀
t : Set ι
hjt : j ∉ t
hst : Disjoint (↑s₀) (insert j t)
ih : Disjoint (⨆ i ∈ s₀, f i) (f j ⊔ ⨆ i ∈ t, f i)
this : Disjoint (f j) ((⨆ i ∈ t, f i) ⊔ ⨆ i ∈ ↑s₀, f i)
⊢ Disjoint (⨆ i ∈ insert j s₀, f i) (⨆ i ∈ t, f i)

Tactic:
s₀.iSup_insert j f,

Goal state after:
case insert
α : Type u_1
ι : Type u_3
inst✝¹ : CompleteLattice α
inst✝ : IsModularLattice α
f : ι → α
hf : iSupIndep f
j : ι
s₀ : Finset ι
hj : j ∉ s₀
t : Set ι
hjt : j ∉ t
hst : Disjoint (↑s₀) (insert j t)
ih : Disjoint (⨆ i ∈ s₀, f i) (f j ⊔ ⨆ i ∈ t, f i)
this : Disjoint (f j) ((⨆ i ∈ t, f i) ⊔ ⨆ i ∈ ↑s₀, f i)
⊢ Disjoint (f j ⊔ ⨆ x ∈ s₀, f x) (⨆ i ∈ t, f i)
Module: Mathlib.Algebra.Algebra.Tower

Goal state before:
pp: R : Type u
A : Type w
M : Type v₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
hsur : Function.Surjective ⇑(algebraMap R A)
X : Set M
⊢ restrictScalars R (span A X) = span R X

Tactic:
refine ((span_le_restrictScalars R A X).antisymm fun m hm => ?_).symm

Goal state after:
R : Type u
A : Type w
M : Type v₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
hsur : Function.Surjective ⇑(algebraMap R A)
X : Set M
m : M
hm : m ∈ restrictScalars R (span A X)
⊢ m ∈ span R X