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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
p : Set β
f : r ≼i s
H : ∀ (a : α), f a ∈ p
a : α
x✝ : { x // x ∈ p }
b : β
m : b ∈ p
h : Subrel s (fun x ↦ x ∈ p) ⟨b, m⟩ ((RelEmbedding.codRestrict p f.toRelEmbedding H) a)
a' : α
e : f a' = ↑⟨b, m⟩
⊢ (RelEmbedding.codRestrict p f.toRelEmbedding H) a' = ⟨b, m⟩

Tactic:
subst e

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
p : Set β
f : r ≼i s
H : ∀ (a : α), f a ∈ p
a : α
x✝ : { x // x ∈ p }
a' : α
m : f a' ∈ p
h : Subrel s (fun x ↦ x ∈ p) ⟨f a', m⟩ ((RelEmbedding.codRestrict p f.toRelEmbedding H) a)
⊢ (RelEmbedding.codRestrict p f.toRelEmbedding H) a' = ⟨f a', m⟩
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : PartialOrder α
f : α ≤i β
⊢ (∃ c ≤ a, f c = b) → b ≤ f a

Tactic:
rintro ⟨c, hc, rfl⟩

Goal state after:
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
inst✝ : PartialOrder α
f : α ≤i β
c : α
hc : c ≤ a
⊢ f c ≤ f a
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : PartialOrder α
f : α ≤i β
⊢ (∃ a' < a, f a' = b) → b < f a

Tactic:
rintro ⟨c, hc, rfl⟩

Goal state after:
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
inst✝ : PartialOrder α
f : α ≤i β
c : α
hc : c < a
⊢ f c < f a
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLinearOrder β
f g : α → β
hf : ωScottContinuous f
hg : ωScottContinuous g
c : Chain α
a : β
⊢ (f ⊓ g) (ωSup c) ≤ a ↔ ωSup (c.map { toFun := f ⊓ g, monotone' := ⋯ }) ≤ a

Tactic:
simp only [Pi.inf_apply, hf.map_ωSup c, hg.map_ωSup c, inf_le_iff, ωSup_le_iff, Chain.coe_map,
    Function.comp, OrderHom.coe_mk, ← forall_or_left, ← forall_or_right]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLinearOrder β
f g : α → β
hf : ωScottContinuous f
hg : ωScottContinuous g
c : Chain α
a : β
⊢ (∀ (x x_1 : ℕ), f (c x_1) ≤ a ∨ g (c x) ≤ a) ↔ ∀ (i : ℕ), f (c i) ≤ a ∨ g (c i) ≤ a
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: c c' : Cardinal.{u_1}
| c ≤ c'

Tactic:
rw [← Cardinal.mk_out c, ← Cardinal.mk_out c', le_def]

Goal state after:
c c' : Cardinal.{u_1}
| Nonempty (Quotient.out c ↪ Quotient.out c')
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: α : Type u
β : Type v
c : Cardinal.{max u v}
f : α → β
hf : ∀ (b : β), lift.{v, u} #↑(f ⁻¹' {b}) ≤ c
b : β
⊢ ↑(⇑Equiv.ulift '' (fun x ↦ { down := f x.down }) ⁻¹' {{ down := b }}) ≃ ↑(f ⁻¹' {b})

Tactic:
Equiv.image_eq_preimage_symm

Goal state after:
α : Type u
β : Type v
c : Cardinal.{max u v}
f : α → β
hf : ∀ (b : β), lift.{v, u} #↑(f ⁻¹' {b}) ≤ c
b : β
⊢ ↑(⇑Equiv.ulift.symm ⁻¹' (fun x ↦ { down := f x.down }) ⁻¹' {{ down := b }}) ≃ ↑(f ⁻¹' {b})
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: α : Type u
⊢ ∃ x, WellFoundedLT α

Tactic:
exact ⟨linearOrderOfSTO WellOrderingRel, ⟨WellOrderingRel.isWellOrder.wf⟩⟩

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

Goal state before:
pp: R : Type u_1
M : Type u_3
a b : R
inst✝² : SMul R M
inst✝¹ : Mul R
inst✝ : IsScalarTower R R M
ab : IsSMulRegular M (a * b)
⊢ IsSMulRegular M b

Tactic:
by
  rw [← smul_eq_mul] at ab
  exact ab.of_smul _

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

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

Tactic:
refine sum_le_sum _ _ fun i => ?_

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

Goal state before:
pp: ι α : Type u
A : ι → Set α
s : Set ι
⊢ #↑(⋃ x ∈ s, A x) ≤ #↑s * ⨆ x, #↑(A ↑x)

Tactic:
by
  rw [biUnion_eq_iUnion]
  apply mk_iUnion_le

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

Goal state before:
pp: α : Type u
S T : Set α
⊢ #↑(S ∪ T) + #↑(S ∩ T) = #↑S + #↑T

Tactic:
exact Quot.sound ⟨Equiv.Set.unionSumInter S T⟩

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

Goal state before:
pp: α : Type u
⊢ 1 < #α ↔ ∃ x y, x ≠ y

Tactic:
one_lt_iff_nontrivial,

Goal state after:
α : Type u
⊢ Nontrivial α ↔ ∃ x y, x ≠ y
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case mp
α : Type u
x : α
⊢ (∃ x y, x ≠ y ∧ {x, y} = univ) → ∃! y, y ≠ x

Tactic:
rintro ⟨a, b, hne, h⟩

Goal state after:
case mp
α : Type u
x a b : α
hne : a ≠ b
h : {a, b} = univ
⊢ ∃! y, y ≠ x
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), a * 0 = 0

Tactic:
intros; ext; exact mul_zero _

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:
rw [← h₁ (g (x + y)), ← h₁ (g x + g y)]

Goal state after:
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 (f (g (x + y))) = g (f (g x + g y))
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 R₂
inst✝¹¹ : Semiring R₃
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommGroup N₂
inst✝⁶ : AddCommGroup N₃
inst✝⁵ : Module R₁ M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
inst✝² : Module R₂ N₂
inst✝¹ : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f g : M →ₛₗ[σ₁₂] N₂
r : R₁
x : M
⊢ (⇑f - ⇑g) (r • x) = σ₁₂ r • (⇑f - ⇑g) x

Tactic:
simp [Pi.sub_apply, smul_sub]

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

Goal state before:
pp: case fst
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝ : M × N
⊢ (0 • x✝).1 = 0.1

Tactic:
exact zero_smul ..

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

Goal state before:
pp: case snd
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝ : M × N
⊢ (0 • x✝).2 = 0.2

Tactic:
exact zero_smul ..

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

Goal state before:
pp: case fst
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
R : Type u_5
inst✝⁴ : Zero R
inst✝³ : Zero M
inst✝² : Zero N
inst✝¹ : SMulWithZero R M
inst✝ : SMulWithZero R N
x✝ : M × N
⊢ (0 • x✝).1 = 0.1

Tactic:
exact zero_smul ..

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

Goal state before:
pp: case snd
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
R : Type u_5
inst✝⁴ : Zero R
inst✝³ : Zero M
inst✝² : Zero N
inst✝¹ : SMulWithZero R M
inst✝ : SMulWithZero R N
x✝ : M × N
⊢ (0 • x✝).2 = 0.2

Tactic:
exact zero_smul ..

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✝⁹ : Semiring R₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : Module R M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
p✝ p' : Submodule R M
q q' : Submodule R₂ M₂
x✝ : M
σ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
f : M →ₛₗ[σ₁₂] M₂
p : Submodule R₂ M₂
a : R
x : M
h : x ∈ ⇑f ⁻¹' ↑p
⊢ a • x ∈ ⇑f ⁻¹' ↑p

Tactic:
simp [p.smul_mem (σ₁₂ a) h, map_smulₛₗ _]

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✝⁹ : Semiring R₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : Module R M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
p✝ p' : Submodule R M
q q' : Submodule R₂ M₂
x✝ : M
σ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
f : M →ₛₗ[σ₁₂] M₂
p : Submodule R₂ M₂
a : R
x : M
h : x ∈ ⇑f ⁻¹' ↑p
⊢ a • x ∈ ⇑f ⁻¹' ↑p

Tactic:
by simp [p.smul_mem (σ₁₂ a) h, map_smulₛₗ _]

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

Goal state before:
pp: case zero
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
f : M →ₗ[R] M
h : p ≤ comap f p
⊢ p ≤ comap (f ^ 0) p

Tactic:
simp [Module.End.one_eq_id]

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

Goal state before:
pp: R : Type u_2
inst✝¹ : Ring R
inst✝ : CharZero R
u : Rˣ
⊢ u ≠ -u

Tactic:
ne_eq,

Goal state after:
R : Type u_2
inst✝¹ : Ring R
inst✝ : CharZero R
u : Rˣ
⊢ ¬u = -u
Module: Mathlib.Algebra.Group.Subsemigroup.Membership

Goal state before:
pp: M : Type u_2
inst✝ : Mul M
S : Set (Subsemigroup M)
hS : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) S
x : M
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

Tactic:
by
  simp only [sSup_eq_iSup', mem_iSup_of_directed hS.directed_val, SetCoe.exists, exists_prop]

Goal state after:
Module: Mathlib.Algebra.Group.Subsemigroup.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝² : Mul M
inst✝¹ : Mul N
ι : Sort u_5
inst✝ : Nonempty ι
f : M →ₙ* N
hf : Function.Injective ⇑f
s : ι → Subsemigroup M
⊢ map f (iInf s) = ⨅ i, map f (s i)

Tactic:
by
  apply SetLike.coe_injective
  simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ s)

Goal state after:
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝⁴ : NonUnitalNonAssocSemiring R
inst✝³ : NonUnitalNonAssocSemiring S
F : Type u_1
inst✝² : FunLike F R S
inst✝¹ : NonUnitalRingHomClass F R S
ι : Sort u_2
inst✝ : Nonempty ι
f : F
hf : Function.Injective ⇑f
s : ι → NonUnitalSubsemiring R
⊢ map f (iInf s) = ⨅ i, map f (s i)

Tactic:
by
  apply SetLike.coe_injective
  simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ s)

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : FaithfulSMul R A
G : Type u_3
inst✝³ : Monoid G
inst✝² : MulSemiringAction G A
inst✝¹ : SMul G R
inst✝ : SMulDistribClass G R A
x✝² x✝¹ : G
x✝ : R
⊢ (x✝² * x✝¹) • x✝ = x✝² • x✝¹ • x✝

Tactic:
apply FaithfulSMul.algebraMap_injective R A
    rw [algebraMap.smul', algebraMap.smul', algebraMap.smul', mul_smul]

Goal state after:
Module: Mathlib.RingTheory.NonUnitalSubring.Basic

Goal state before:
pp: F : Type w
R : Type u
S : Type v
inst✝⁴ : NonUnitalNonAssocRing R
inst✝³ : NonUnitalNonAssocRing S
inst✝² : FunLike F R S
inst✝¹ : NonUnitalRingHomClass F R S
ι : Sort u_1
inst✝ : Nonempty ι
f : F
hf : Function.Injective ⇑f
s : ι → NonUnitalSubring R
⊢ map f (iInf s) = ⨅ i, map f (s i)

Tactic:
by
  apply SetLike.coe_injective
  simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ s)

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

Goal state before:
pp: R : Type u
S : Type v
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
ι : Sort u_1
inst✝ : Nonempty ι
f : R →+* S
hf : Function.Injective ⇑f
s : ι → Subsemiring R
⊢ map f (iInf s) = ⨅ i, map f (s i)

Tactic:
by
  apply SetLike.coe_injective
  simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ s)

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

Goal state before:
pp: R : Type u
S : Type v
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
ι : Sort u_1
inst✝ : Nonempty ι
f : R →+* S
hf : Function.Injective ⇑f
s : ι → Subring R
⊢ map f (iInf s) = ⨅ i, map f (s i)

Tactic:
by
  apply SetLike.coe_injective
  simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ s)

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

Goal state before:
pp: case mpr
M : Type u_1
inst✝ : CommMonoid M
a b : M
⊢ (∃ c, b = a * c) → ∃ x, a * x ~ᵤ b

Tactic:
rintro ⟨c, rfl⟩

Goal state after:
case mpr
M : Type u_1
inst✝ : CommMonoid M
a c : M
⊢ ∃ x, a * x ~ᵤ a * c
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case succ.inl
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 : p * q ∣ p * p ^ n
⊢ ∃ i, i ≤ n + 1 ∧ p * q ~ᵤ p ^ i

Tactic:
rw [mul_dvd_mul_iff_left hp.ne_zero, ih] at h

Goal state after:
case succ.inl
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 : ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
⊢ ∃ i, i ≤ n + 1 ∧ p * q ~ᵤ p ^ i
Module: Mathlib.Algebra.Algebra.Equiv

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

Tactic:
have : IsLocalHom e.toRingEquiv := inferInstance
  exact ⟨this.map_nonunit⟩

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₂
f : M →ₛₗ[τ₁₂] M₂
h : ∀ (u v : ↥f.ker →ₗ[R] M), f ∘ₛₗ u = f ∘ₛₗ v → u = v
⊢ f.ker = ⊥

Tactic:
have h₁ : f.comp (0 : ker f →ₗ[R] M) = 0 := comp_zero _
  rw [← Submodule.range_subtype (ker f),
    ← h 0 (ker f).subtype (Eq.trans h₁ (comp_ker_subtype f).symm)]
  exact range_zero

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
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst✝¹² : Semiring R
inst✝¹¹ : Semiring R₂
inst✝¹⁰ : Semiring R₃
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : Module R M
inst✝⁵ : Module R₂ M₂
inst✝⁴ : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝³ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
inst✝² : RingHomSurjective τ₁₂
inst✝¹ : RingHomSurjective τ₂₃
inst✝ : RingHomSurjective τ₁₃
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
hf : f.range = ⊤
⊢ (g ∘ₛₗ f).range = g.range

Tactic:
rw [range_comp, hf, Submodule.map_top]

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

Goal state before:
pp: case mp
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
x✝ : M
hx : ∀ p ∈ {p | ∀ ⦃r : S⦄ {n : M}, r ∈ ∅ → n ∈ N → r • n ∈ p}, x✝ ∈ p
⊢ x✝ ∈ ⊥

Tactic:
exact hx ⊥ (fun r _ hr ↦ hr.elim)

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z : α
hxy : x ≤ y
hinf : y ⊓ z ≤ x
hsup : y ≤ x ⊔ z
⊢ x = y

Tactic:
refine hxy.antisymm ?_

Goal state after:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z : α
hxy : x ≤ y
hinf : y ⊓ z ≤ x
hsup : y ≤ x ⊔ z
⊢ y ≤ x
Module: Mathlib.Data.Finset.Lattice.Prod

Goal state before:
pp: α : Type u_2
ι : Type u_5
κ : Type u_6
inst✝ : DistribLattice α
s : Finset ι
t : Finset κ
hs : s.Nonempty
ht : t.Nonempty
f : ι → α
g : κ → α
⊢ s.sup' hs f ⊓ t.sup' ht g = (s ×ˢ t).sup' ⋯ fun i ↦ f i.1 ⊓ g i.2

Tactic:
simp_rw [Finset.sup'_inf_distrib_right, Finset.sup'_inf_distrib_left, sup'_product_left]

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

Goal state before:
pp: M : Type u_4
inst✝ : AddCommMonoid M
s : Set M
⊢ (span ℕ s).toAddSubmonoid = AddSubmonoid.closure s

Tactic:
refine Eq.symm (AddSubmonoid.closure_eq_of_le subset_span ?_)

Goal state after:
M : Type u_4
inst✝ : AddCommMonoid M
s : Set M
⊢ (span ℕ s).toAddSubmonoid ≤ AddSubmonoid.closure s
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : IsCoatomistic α
b : α
⊢ b = ⊤ ∨ ∃ a, IsCoatom a ∧ b ≤ a

Tactic:
by
    rcases isGLB_coatoms b with ⟨s, hsb, hs⟩
    rcases s.eq_empty_or_nonempty with rfl | ⟨a, ha⟩
    · simp_all
    · exact Or.inr ⟨a, hs _ ha, hsb.1 ha⟩

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inr.inl
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ equivBool ⊤ ≤ equivBool ⊥ ↔ ⊤ ≤ ⊥

pp: case inr.inr
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ equivBool ⊤ ≤ equivBool ⊤ ↔ ⊤ ≤ ⊤

Tactic:
· simp [bot_ne_top.symm, Bool.false_lt_true]

Goal state after:
case inr.inr
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ equivBool ⊤ ≤ equivBool ⊤ ↔ ⊤ ≤ ⊤
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 : Submodule R M
⊢ IsPrincipal R ↥p ↔ p.IsPrincipal

Tactic:
simp_rw [IsPrincipal, isPrincipal_iff]

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ (∃ a, ⊤ = R ∙ a) ↔ ∃ a, p = R ∙ a
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : BoundedOrder α
inst✝ : BoundedOrder β
f : α ≃o β
⊢ IsSimpleOrder α ↔ IsSimpleOrder β

Tactic:
isSimpleOrder_iff_isAtom_top,

Goal state after:
α : Type u_2
β : Type u_3
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : BoundedOrder α
inst✝ : BoundedOrder β
f : α ≃o β
⊢ IsAtom ⊤ ↔ IsSimpleOrder β
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : BoundedOrder α
inst✝ : BoundedOrder β
f : α ≃o β
⊢ IsAtom ⊤ ↔ IsSimpleOrder β

Tactic:
isSimpleOrder_iff_isAtom_top,

Goal state after:
α : Type u_2
β : Type u_3
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : BoundedOrder α
inst✝ : BoundedOrder β
f : α ≃o β
⊢ IsAtom ⊤ ↔ IsAtom ⊤
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝⁴ : Lattice α
inst✝³ : BoundedOrder α
inst✝² : IsModularLattice α
inst✝¹ : ComplementedLattice α
inst✝ : IsAtomic α
x y : α
xy : IsCompl x y
⊢ (∃ a, IsAtom a ∧ a ≤ y) → ∃ a, IsCoatom a ∧ x ≤ a

Tactic:
· rintro ⟨a, ha, ay⟩
      rcases exists_isCompl (xy.symm.IicOrderIsoIci ⟨a, ay⟩) with ⟨⟨b, xb⟩, hb⟩
      refine ⟨↑(⟨b, xb⟩ : Set.Ici x), IsCoatom.of_isCoatom_coe_Ici ?_, xb⟩
      rw [← hb.isAtom_iff_isCoatom, OrderIso.isAtom_iff]
      apply ha.Iic

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
p : Prop
⊢ p = ⊥ ∨ p = ⊤

Tactic:
by simp [em']

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
⊢ (s.sigma g).SupIndep f ↔ (s.SupIndep fun i ↦ (g i).sup fun b ↦ f ⟨i, b⟩) ∧ ∀ i ∈ s, (g i).SupIndep fun b ↦ f ⟨i, b⟩

Tactic:
refine ⟨fun h ↦ ⟨fun t _ i _ _ ↦ ?_, fun i _ t _ j _ _ ↦ ?_⟩, fun h ↦ h.1.sigma h.2⟩

Goal state after:
case refine_1
α : Type u_1
ι : Type u_3
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
h : (s.sigma g).SupIndep f
t : Finset ι
x✝² : t ⊆ s
i : ι
x✝¹ : i ∈ s
x✝ : i ∉ t
⊢ Disjoint ((fun i ↦ (g i).sup fun b ↦ f ⟨i, b⟩) i) (t.sup fun i ↦ (g i).sup fun b ↦ f ⟨i, b⟩)

case refine_2
α : Type u_1
ι : Type u_3
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
h : (s.sigma g).SupIndep f
i : ι
x✝³ : i ∈ s
t : Finset (β i)
x✝² : t ⊆ g i
j : β i
x✝¹ : j ∈ g i
x✝ : j ∉ t
⊢ Disjoint ((fun b ↦ f ⟨i, b⟩) j) (t.sup fun b ↦ f ⟨i, b⟩)
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case inr
α : 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 ≠ ⊥
⊢ Disjoint (t i) (⨆ j, ⨆ (_ : j ≠ i), t j)

Tactic:
| inr hi =>

Goal state after:
case inr
α : 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 ≠ ⊥
⊢ Disjoint (t i) (⨆ j, ⨆ (_ : j ≠ i), t j)
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝¹ : CompleteLattice α
inst✝ : IsModularLattice α
f : ι → α
t : Set ι
hf : iSupIndep f
⊢ ∀ (s : Finset ι), Disjoint (↑s) t → Disjoint (⨆ i ∈ s, f i) (⨆ i ∈ t, f i)

Tactic:
intro s hst

Goal state after:
α : Type u_1
ι : Type u_3
inst✝¹ : CompleteLattice α
inst✝ : IsModularLattice α
f : ι → α
t : Set ι
hf : iSupIndep f
s : Finset ι
hst : Disjoint (↑s) t
⊢ Disjoint (⨆ i ∈ s, f i) (⨆ i ∈ t, f i)
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: case e'_1.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
f g : M →ₗ[R] N
S : Set M
hM : span R S = ⊤
⊢ f ∘ₗ ⊤.subtype = g ∘ₗ ⊤.subtype → f = g

Tactic:
intro h
    ext x
    exact DFunLike.congr_fun h ⟨x, by simp⟩

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

Goal state before:
pp: R : Type u_1
M : Type u_4
S : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring S
inst✝² : SMul R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
p : Submodule R M
q : Submodule S M
h₁ : p ≤ restrictScalars R q
h₂ : q ≤ span S ↑p
⊢ span S (⇑q.subtype '' range ⇑(inclusion h₁)) = q

Tactic:
suffices q.subtype '' ((LinearMap.range (inclusion h₁)) : Set <| q.restrictScalars R) = p by
    refine this ▸ le_antisymm ?_ h₂
    simpa using span_mono (R := S) h₁

Goal state after:
R : Type u_1
M : Type u_4
S : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring S
inst✝² : SMul R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
p : Submodule R M
q : Submodule S M
h₁ : p ≤ restrictScalars R q
h₂ : q ≤ span S ↑p
⊢ ⇑q.subtype '' ↑(inclusion h₁).range = ↑p