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

Goal state before:
pp: case inl
α : Type u_2
c : Chain (Part α)
a b : α
i : ℕ
ha : a ∈ c i
j : ℕ
hb : b ∈ c j
hij : i ≤ j
this : a ∈ c.toOrderHom j
⊢ a = b

Tactic:
apply mem_unique this hb

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
f : ι → α → β
hf : ∀ (i : ι), ωScottContinuous (f i)
⊢ ωScottContinuous (⨆ i, f i)

Tactic:
by
  refine ωScottContinuous.of_monotone_map_ωSup
    ⟨Monotone.iSup fun i ↦ (hf i).monotone, fun c ↦ eq_of_forall_ge_iff fun a ↦ ?_⟩
  simp +contextual [ωSup_le_iff, (hf _).map_ωSup, @forall_comm ι]

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ a ∈ ωSup (c.map f), ωSup (c.map g) a ≤ x
⊢ ∀ (i : ℕ), (c.map (f.partBind g)) i ≤ x

Tactic:
intro i y hy
    simp only [Part.mem_bind_iff, Chain.coe_map,
      Function.comp_apply, OrderHom.partBind_coe] at hy
    rcases hy with ⟨b, hb₀, hb₁⟩
    apply h''' b _
    · apply le_ωSup (c.map g) _ _ _ hb₁
    · apply le_ωSup (c.map f) i _ hb₀

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

Goal state before:
pp: case refine_2
α β : Type u
a : Cardinal.{u}
b : Cardinal.{max u v}
⊢ b < (OrderEmbedding.ofMapLEIff lift.{v, u} ⋯).ltEmbedding a →
    b ∈ Set.range ⇑(OrderEmbedding.ofMapLEIff lift.{v, u} ⋯).ltEmbedding

Tactic:
refine inductionOn₂ a b fun α β h ↦ ?_

Goal state after:
case refine_2
α✝ β✝ : Type u
a : Cardinal.{u}
b : Cardinal.{max u v}
α : Type u
β : Type (max u v)
h : #β < (OrderEmbedding.ofMapLEIff lift.{v, u} ⋯).ltEmbedding #α
⊢ #β ∈ Set.range ⇑(OrderEmbedding.ofMapLEIff lift.{v, u} ⋯).ltEmbedding
Module: Mathlib.SetTheory.Cardinal.SchroederBernstein

Goal state before:
pp: α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
⊢ ∃ h, Bijective h

Tactic:
obtain ⟨f, hf, _⟩ := schroeder_bernstein_of_rel hf hg (fun x y ↦ True) (by simp) (by simp)
  exact ⟨f, hf⟩

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

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

Tactic:
simp only [Chain.coe_map, OrderHomClass.coe_coe, comp_apply]

Goal state after:
case a
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
n : ℕ
⊢ f ((iterateChain (↑f) x h) n) ≤ ωSup (iterateChain (↑f) x h)
Module: Mathlib.Order.OmegaCompletePartialOrder

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

Tactic:
rintro (_ | n)

Goal state after:
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)

case a.succ
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
n : ℕ
⊢ (iterateChain (↑f) x h) (n + 1) ≤ ωSup ((iterateChain (↑f) x h).map ↑f)
Module: Mathlib.Algebra.Group.Hom.CompTypeclasses

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
σ : M →* M
h : _root_.CompTriple.IsId ⇑σ
x✝ : M
⊢ σ x✝ = (id M) x✝

Tactic:
exact congr_fun h.eq_id _

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

Goal state before:
pp: α : Type u
n : ℕ
H : ∀ (s : Finset α), s.card ≤ n
⊢ #α ≤ ↑n

Tactic:
by
  contrapose! H
  apply exists_finset_le_card α (n + 1)
  simpa using H

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

Goal state before:
pp: α : Type u
A B : Set α
hfin : B.Finite
hlt : A ⊂ B
this : Fintype ↑A
⊢ #↑A < #↑B

Tactic:
have : Fintype B := hfin.fintype

Goal state after:
α : Type u
A B : Set α
hfin : B.Finite
hlt : A ⊂ B
this✝ : Fintype ↑A
this : Fintype ↑B
⊢ #↑A < #↑B
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
S T : Set α
h : #↑S < #↑T
⊢ (T \ S).Nonempty

Tactic:
by
  rw [← mk_set_ne_zero_iff]
  intro h'
  exact h.not_ge ((le_mk_sdiff_add_mk T S).trans (by simp [h']))

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✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
x : R
y z : A
⊢ x • y * z = x • (y * z)

Tactic:
smul_def,

Goal state after:
R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
x : R
y z : A
⊢ (algebraMap R A) x * y * z = x • (y * z)
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✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
x : R
y z : A
⊢ (algebraMap R A) x * y * z = x • (y * z)

Tactic:
smul_def,

Goal state after:
R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
x : R
y z : A
⊢ (algebraMap R A) x * y * z = (algebraMap R A) x * (y * z)
Module: Mathlib.Algebra.Algebra.Defs

Goal state before:
pp: R : Type u
A : Type w
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : R
x y : A
⊢ x * s • y = s • (x * y)

Tactic:
smul_def,

Goal state after:
R : Type u
A : Type w
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : R
x y : A
⊢ x * ((algebraMap R A) s * y) = s • (x * y)
Module: Mathlib.Algebra.Algebra.Defs

Goal state before:
pp: R : Type u
A : Type w
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : R
x y : A
⊢ x * ((algebraMap R A) s * y) = s • (x * y)

Tactic:
smul_def,

Goal state after:
R : Type u
A : Type w
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : R
x y : A
⊢ x * ((algebraMap R A) s * y) = (algebraMap R A) s * (x * y)
Module: Mathlib.Algebra.Module.Hom

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
M✝ : Type u_3
A : Type u_4
B : Type u_5
S : Type u_6
M : Type u_7
M₂ : Type u_8
inst✝³ : Semiring S
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module S M
s s' : Sᵈᵐᵃ
f : M →+ M₂
m : M
⊢ ((s + s') • f) m = (s • f + s' • f) m

Tactic:
simp_rw [AddMonoidHom.add_apply, DomMulAct.smul_addMonoidHom_apply, ← map_add, ← add_smul]; rfl

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
X : Type u_4
Y : Type u_5
σ : M → N
inst✝ : Monoid M
f : M →ₑ[id] M
m : M
⊢ MulOpposite.op m • f 1 = f m

Tactic:
simp [← map_smul]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
X : Type u_4
Y : Type u_5
σ : M → N
inst✝ : Monoid M
f g : M →ₑ[id] M
⊢ (f * g) 1 = MulOpposite.op (g 1) • f 1

Tactic:
simp [← map_smul]

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

Goal state before:
pp: R : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R'
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : Module R M
inst✝⁶ : Module R' M'
σ₁₂ : R →+* R'
S' : Type u_6
T' : Type u_7
inst✝⁵ : Monoid S'
inst✝⁴ : DistribMulAction S' M
inst✝³ : SMulCommClass R S' M
inst✝² : Monoid T'
inst✝¹ : DistribMulAction T' M
inst✝ : SMulCommClass R T' M
a : S'ᵈᵐᵃ
f : M →ₛₗ[σ₁₂] M'
c : R
x : M
⊢ f (c • DomMulAct.mk.symm a • x) = σ₁₂ c • f (DomMulAct.mk.symm a • x)

Tactic:
f.map_smulₛₗ

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝⁴ : FunLike F α β
inst✝³ : CompleteLattice α
inst✝² : CompleteLattice β
inst✝¹ : CompleteLattice γ
inst✝ : CompleteLattice δ
f g : FrameHom α β
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := f
    obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := g
    congr

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝¹ : FunLike F α β
inst✝ : CompleteLattice α
x : α × α
s : Set (α × α)
⊢ (sInf s).1 ⊓ (sInf s).2 = sInf ((fun x ↦ x.1 ⊓ x.2) '' s)

Tactic:
by simp_rw [Prod.fst_sInf, Prod.snd_sInf, sInf_image, iInf_inf_eq]

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝³ : Semiring R
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
e : M ≃ₛₗ[σ₁₂] M₂
p : Submodule R M
y' : M₂
hy✝ : y' ∈ Submodule.map (↑e) p
hy : ∃ y ∈ p, ↑e y = y'
⊢ ↑e.symm ↑⟨y', hy✝⟩ ∈ p

Tactic:
rcases hy with ⟨x, hx, hxy⟩

Goal state after:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝³ : Semiring R
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
e : M ≃ₛₗ[σ₁₂] M₂
p : Submodule R M
y' : M₂
hy : y' ∈ Submodule.map (↑e) p
x : M
hx : x ∈ p
hxy : ↑e x = y'
⊢ ↑e.symm ↑⟨y', hy⟩ ∈ p
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₁ ∈ closure (⋃ i, ↑(S i))
mem : ∀ (i : ι), ∀ x₂ ∈ S i, C x₂
mul : ∀ (x y : M), C x → C y → C (x * y)
x₂ : M
hx₂ : x₂ ∈ ⋃ i, ↑(S i)
⊢ C x₂

Tactic:
obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hx₂

Goal state after:
ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
C : M → Prop
x₁ : M
hx₁ : x₁ ∈ closure (⋃ i, ↑(S i))
mem : ∀ (i : ι), ∀ x₂ ∈ S i, C x₂
mul : ∀ (x y : M), C x → C y → C (x * y)
x₂ : M
hx₂ : x₂ ∈ ⋃ i, ↑(S i)
i : ι
hi : x₂ ∈ ↑(S i)
⊢ C x₂
Module: Mathlib.Algebra.Algebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₗ[R] B
a : A
r : R
⊢ f (a * (algebraMap R A) r) = f a * (algebraMap R B) r

Tactic:
by
  rw [← Algebra.commutes, ← Algebra.commutes, map_algebraMap_mul]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
r : R
⊢ (↑↑(algebraMap S A)).toFun ((algebraMap R S) r) = (algebraMap R A) r

Tactic:
simpa [Algebra.smul_def] using smul_assoc r (1 : S) (1 : A)

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : M
hp : Prime p
a b : M
k l : ℕ
x✝³ : p ^ k ∣ a
x✝² : p ^ l ∣ b
x✝¹ : p ^ (k + l + 1) ∣ a * b
x : M
hx : a = p ^ k * x
y : M
hy : b = p ^ l * y
z : M
hz : a * b = p ^ (k + l + 1) * z
h : p ^ (k + l) * (x * y) = p ^ (k + l) * (p * z)
hp0 : p ^ (k + l) ≠ 0
hpd : p ∣ x * y
x✝ : p ∣ x
d : M
hd : x = p * d
⊢ a = p ^ (k + 1) * d

Tactic:
simp [*, pow_succ, mul_comm, mul_left_comm, mul_assoc]

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : M
hp : Prime p
a b : M
k l : ℕ
x✝³ : p ^ k ∣ a
x✝² : p ^ l ∣ b
x✝¹ : p ^ (k + l + 1) ∣ a * b
x : M
hx : a = p ^ k * x
y : M
hy : b = p ^ l * y
z : M
hz : a * b = p ^ (k + l + 1) * z
h : p ^ (k + l) * (x * y) = p ^ (k + l) * (p * z)
hp0 : p ^ (k + l) ≠ 0
hpd : p ∣ x * y
x✝ : p ∣ y
d : M
hd : y = p * d
⊢ b = p ^ (l + 1) * d

Tactic:
simp [*, pow_succ, mul_comm, mul_left_comm, mul_assoc]

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

Goal state before:
pp: R : Type u_2
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
inst✝ : Subsingleton Rˣ
p₁ p₂ : R
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₁
h : p₁ ^ k₁ = p₂ ^ k₂
⊢ p₁ = p₂

Tactic:
rw [← associated_iff_eq] at h ⊢

Goal state after:
R : Type u_2
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
inst✝ : Subsingleton Rˣ
p₁ p₂ : R
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₁
h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂
⊢ p₁ ~ᵤ p₂
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: R : Type u_2
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
inst✝ : Subsingleton Rˣ
p₁ p₂ : R
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₂
h : p₁ ^ k₁ = p₂ ^ k₂
⊢ p₁ = p₂

Tactic:
rw [← associated_iff_eq] at h ⊢

Goal state after:
R : Type u_2
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
inst✝ : Subsingleton Rˣ
p₁ p₂ : R
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₂
h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂
⊢ p₁ ~ᵤ p₂
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
a b : Associates M
⊢ a ≤ b * a

Tactic:
rw [mul_comm]; exact le_mul_right

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₂
hf : Surjective ⇑f
p q : Submodule R M
hpq : Codisjoint p q
⊢ Codisjoint (map f p) (map f q)

Tactic:
by
  rw [codisjoint_iff, ← Submodule.map_sup, codisjoint_iff.mp hpq, map_top,
    LinearMap.range_eq_top_of_surjective f hf]

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M₁ →ₗ[R] M₂ →ₗ[R] M
i : M₃ →ₗ[R] M
hi : Injective ⇑i
hf : ∀ (x : M₁) (y : M₂), (f x) y ∈ i.range
e : ↥i.range ≃ₗ[R] M₃ := (LinearEquiv.ofInjective i hi).symm
x₁ x₂ : M₁
⊢ ↑e ∘ₗ codRestrict i.range (f (x₁ + x₂)) ⋯ = ↑e ∘ₗ codRestrict i.range (f x₁) ⋯ + ↑e ∘ₗ codRestrict i.range (f x₂) ⋯

Tactic:
ext y

Goal state after:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M₁ →ₗ[R] M₂ →ₗ[R] M
i : M₃ →ₗ[R] M
hi : Injective ⇑i
hf : ∀ (x : M₁) (y : M₂), (f x) y ∈ i.range
e : ↥i.range ≃ₗ[R] M₃ := (LinearEquiv.ofInjective i hi).symm
x₁ x₂ : M₁
y : M₂
⊢ (↑e ∘ₗ codRestrict i.range (f (x₁ + x₂)) ⋯) y =
    (↑e ∘ₗ codRestrict i.range (f x₁) ⋯ + ↑e ∘ₗ codRestrict i.range (f x₂) ⋯) y
Module: Mathlib.Algebra.Module.Submodule.Equiv

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M₁ →ₗ[R] M₂ →ₗ[R] M
i : M₃ →ₗ[R] M
hi : Injective ⇑i
hf : ∀ (x : M₁) (y : M₂), (f x) y ∈ i.range
e : ↥i.range ≃ₗ[R] M₃ := (LinearEquiv.ofInjective i hi).symm
t : R
x : M₁
⊢ ↑e ∘ₗ codRestrict i.range (f (t • x)) ⋯ = (RingHom.id R) t • ↑e ∘ₗ codRestrict i.range (f x) ⋯

Tactic:
ext y

Goal state after:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M₁ →ₗ[R] M₂ →ₗ[R] M
i : M₃ →ₗ[R] M
hi : Injective ⇑i
hf : ∀ (x : M₁) (y : M₂), (f x) y ∈ i.range
e : ↥i.range ≃ₗ[R] M₃ := (LinearEquiv.ofInjective i hi).symm
t : R
x : M₁
y : M₂
⊢ (↑e ∘ₗ codRestrict i.range (f (t • x)) ⋯) y = ((RingHom.id R) t • ↑e ∘ₗ codRestrict i.range (f x) ⋯) y
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
N : Submodule R M
s t : Set S
⊢ ∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s ⊔ t → n ∈ N → r • n ∈ s • N ⊔ t • N

Tactic:
by rintro _ _ (hr | hr) hn
        · exact Submodule.mem_sup_left (mem_set_smul_of_mem_mem hr hn)
        · exact Submodule.mem_sup_right (mem_set_smul_of_mem_mem hr hn)

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 : Set M
⊢ span R s = ⨆ x ∈ s, R ∙ x

Tactic:
simp only [← span_iUnion, Set.biUnion_of_singleton s]

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝ : PartialOrder α
b : α
a : ↑(Iic b)
⊢ IsCoatom a ↔ ↑a ⋖ b

Tactic:
rw [← covBy_top_iff]

Goal state after:
α : Type u_2
inst✝ : PartialOrder α
b : α
a : ↑(Iic b)
⊢ a ⋖ ⊤ ↔ ↑a ⋖ b
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case refine_2
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
⊢ ∃ a, a • y = 0

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

pp: case refine_4
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
⊢ ∀ (a : R), ∀ x ∈ R ∙ y, (∃ a, a • y = x) → ∃ a_2, a_2 • y = a • x

Tactic:
· exact ⟨0, by simp⟩

Goal state after:
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

case refine_4
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
⊢ ∀ (a : R), ∀ x ∈ R ∙ y, (∃ a, a • y = x) → ∃ a_2, a_2 • y = a • x
Module: Mathlib.Order.SupClosed

Goal state before:
pp: case sup
α : Type u_3
β : Type u_4
inst✝¹ : Lattice α
inst✝ : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
a b : α
ha : a ∈ f ⁻¹' latticeClosure (f '' s)
hb : b ∈ f ⁻¹' latticeClosure (f '' s)
⊢ a ⊔ b ∈ f ⁻¹' latticeClosure (f '' s)

Tactic:
simpa [map_sup] using isSublattice_latticeClosure.supClosed ha hb

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case refine_1
ι✝ : Sort u_1
α : Type u_2
β : Type u_3
ι : Type u_4
π : ι → Type u
inst✝² : (i : ι) → PartialOrder (π i)
inst✝¹ : (i : ι) → OrderBot (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
i : ι
⊢ s i ∈ upperBounds (Function.eval i '' {f | (∃ i a, IsAtom a ∧ f = Function.update ⊥ i a) ∧ f ≤ s})

Tactic:
rintro _ ⟨_, ⟨⟨_, _, _, rfl⟩, hs⟩, rfl⟩
      exact hs i

Goal state after:
Module: Mathlib.Order.Atoms

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

Tactic:
rw [isAtom_iff_le_of_ge, bot_eq_empty, ← nonempty_iff_ne_empty]

Goal state after:
α : Type u_2
s : Set α
⊢ (s.Nonempty ∧ ∀ (b : Set α), b ≠ ∅ → b ⊆ s → s ⊆ b) → ∃ x, s = {x}
Module: Mathlib.Order.CompactlyGenerated.Basic

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

Tactic:
rw [isCompactElement_iff_le_of_directed_sSup_le]

Goal state after:
α : Type u_2
inst✝ : CompleteLattice α
k : α
⊢ (∀ (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.Algebra.BigOperators.GroupWithZero.Finset

Goal state before:
pp: case insert
ι : Type u_1
M₀ : Type u_4
inst✝² : CommMonoidWithZero M₀
f : ι → M₀
s : Finset ι
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
a✝ : ι
s✝ : Finset ι
ha : a✝ ∉ s✝
ih : ∏ x ∈ s✝, f x = 0 ↔ ∃ a ∈ s✝, f a = 0
⊢ f a✝ = 0 ∨ ∏ x ∈ s✝, f x = 0 ↔ ∃ a ∈ insert a✝ s✝, f a = 0

Tactic:
exists_mem_insert,

Goal state after:
case insert
ι : Type u_1
M₀ : Type u_4
inst✝² : CommMonoidWithZero M₀
f : ι → M₀
s : Finset ι
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
a✝ : ι
s✝ : Finset ι
ha : a✝ ∉ s✝
ih : ∏ x ∈ s✝, f x = 0 ↔ ∃ a ∈ s✝, f a = 0
⊢ f a✝ = 0 ∨ ∏ x ∈ s✝, f x = 0 ↔ f a✝ = 0 ∨ ∃ x ∈ s✝, f x = 0
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 = (⋂ x ∈ s, f x).indicator (∏ i ∈ s, g i) j

Tactic:
Set.indicator

Goal state after:
ι : 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
Module: Mathlib.Algebra.BigOperators.Ring.List

Goal state before:
pp: R : Type u_5
inst✝ : NonUnitalSemiring R
a : R
l : List R
h : ∀ (x : R), x ∈ l → a ∣ x
⊢ a ∣ l.sum

Tactic:
by
  induction l with
  | nil => exact dvd_zero _
  | cons x l ih =>
    rw [List.sum_cons]
    exact dvd_add (h _ mem_cons_self) (ih fun x hx ↦ h x (mem_cons_of_mem _ hx))

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

Goal state before:
pp: α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max : ∀ ⦃t : Set α⦄, t ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} → s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
a : α
ha : a ∈ {a | a ≤ c ∧ IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
x : α
hx : x ∈ s ∪ {a}
⊢ Disjoint x (sSup ((s ∪ {a}) \ {x}))

Tactic:
rw [Set.mem_union, Set.mem_singleton_iff] at hx
    obtain rfl | xa := eq_or_ne x a
    · simp only [Set.mem_singleton, Set.insert_sdiff_of_mem, Set.union_singleton]
      exact con.mono_right ((sSup_le_sSup Set.sdiff_subset).trans le_sup_right)
    · have h : (s ∪ {a}) \ {x} = s \ {x} ∪ {a} := by
        simp only [Set.union_singleton]
        rw [Set.insert_sdiff_of_notMem]
        rw [Set.mem_singleton_iff]
        exact Ne.symm xa
      rw [h, sSup_union, sSup_singleton]
      apply
        (s_ind (hx.resolve_right xa)).disjoint_sup_right_of_disjoint_sup_left
          (a_dis_Sup_s.mono_right _).symm
      rw [← sSup_insert, Set.insert_sdiff_singleton, Set.insert_eq_of_mem (hx.resolve_right xa)]

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

Goal state before:
pp: case inr
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max : ∀ ⦃t : Set α⦄, t ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} → s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
x : α
ha : x ∈ {a | a ≤ c ∧ IsAtom a}
con : Disjoint x (b ⊔ sSup s)
a_dis_Sup_s : Disjoint x (sSup s)
⊢ IsAtom x ∧ x ≤ c

Tactic:
· exact ha.symm

Goal state after: