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
inst✝² : Std.Trichotomous s
inst✝¹ : Std.Irrefl s
inst✝ : IsWellFounded α r
f g : r ≼i s
⊢ f = g

Tactic:
by
    ext a
    refine IsWellFounded.induction r a fun b IH =>
      extensional_of_trichotomous_of_irrefl s fun x => ?_
    rw [f.exists_eq_iff_rel, g.exists_eq_iff_rel]
    exact exists_congr fun x => and_congr_left fun hx => IH _ hx ▸ Iff.rfl

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : IsWellOrder α r
f : r ≺i r
⊢ False

Tactic:
have h := f.lt_top f.top

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝ : IsWellOrder α r
f : r ≺i r
h : r (f.toRelEmbedding f.top) f.top
⊢ False
Module: Mathlib.Order.Hom.Order

Goal state before:
pp: case mpr
α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), f (a₁ ⊔ a₂) ≤ f a₁ ⊔ a₂
n₁ : ℕ
⊢ ∀ (n₂ : ℕ) (a₁ a₂ : α), (⇑f)^[n₁ + n₂] (a₁ ⊔ a₂) ≤ (⇑f)^[n₁] a₁ ⊔ (⇑f)^[n₂] a₂

Tactic:
n₂

Goal state after:
case mpr
α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), f (a₁ ⊔ a₂) ≤ f a₁ ⊔ a₂
n₁ n₂ : ℕ
⊢ ∀ (a₁ a₂ : α), (⇑f)^[n₁ + n₂] (a₁ ⊔ a₂) ≤ (⇑f)^[n₁] a₁ ⊔ (⇑f)^[n₂] a₂
Module: Mathlib.Order.BourbakiWitt

Goal state before:
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 α
hc : ↑c ⊆ {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}
⊢ cSup c ≤ y ∨ f y ≤ cSup c

Tactic:
by_cases! h : ∀ z ∈ c, z ≤ y

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

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

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

Tactic:
exact le_refl (f z)

Goal state after:
Module: Mathlib.Order.Zorn

Goal state before:
pp: case refine_1
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
cs : Set (Set α)
hcs₀ : cs ⊆ {s | c ⊆ s ∧ IsChain r s}
hcs₁ : IsChain (fun x1 x2 ↦ x1 ⊆ x2) cs
s : Set α
hs : s ∈ cs
⊢ ∃ ub ∈ {s | c ⊆ s ∧ IsChain r s}, ∀ s ∈ cs, s ⊆ ub

Tactic:
refine
    ⟨⋃₀cs, ⟨fun _ ha => Set.mem_sUnion_of_mem ((hcs₀ hs).left ha) hs, ?_⟩, fun _ =>
      Set.subset_sUnion_of_mem⟩

Goal state after:
case refine_1
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
cs : Set (Set α)
hcs₀ : cs ⊆ {s | c ⊆ s ∧ IsChain r s}
hcs₁ : IsChain (fun x1 x2 ↦ x1 ⊆ x2) cs
s : Set α
hs : s ∈ cs
⊢ IsChain r (⋃₀ cs)
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: a b : Cardinal.{u_1}
h : a < b
⊢ a + 1 ≤ b

Tactic:
induction a, b using Cardinal.inductionOn₂ with | mk α β
   =>  _ 

Goal state after:
case mk
α β : Type u_1
h : #α < #β
⊢ #α + 1 ≤ #β
Module: Mathlib.SetTheory.Cardinal.ToNat

Goal state before:
pp: c : Cardinal.{u}
⊢ c = 0 ∨ toENat c = ⊤ ↔ c = 0 ∨ ℵ₀ ≤ c

Tactic:
toENat_eq_top

Goal state after:
c : Cardinal.{u}
⊢ c = 0 ∨ ℵ₀ ≤ c ↔ c = 0 ∨ ℵ₀ ≤ c
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: n : ℕ
c : Cardinal.{u_1}
⊢ c < ↑n + 1 ↔ c ≤ ↑n

Tactic:
rw [← Order.lt_succ_iff, succ_natCast]

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_10
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
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 : g ∘ₛₗ f = id
⊢ Injective (⇑g ∘ ⇑f)

Tactic:
← coe_comp,

Goal state after:
R : Type u_1
S : Type u_5
M : Type u_8
M₂ : Type u_10
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
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 : g ∘ₛₗ f = id
⊢ Injective ⇑(g ∘ₛₗ f)
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_10
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
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 : g ∘ₛₗ f = id
⊢ Surjective (⇑g ∘ ⇑f)

Tactic:
← coe_comp,

Goal state after:
R : Type u_1
S : Type u_5
M : Type u_8
M₂ : Type u_10
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
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 : g ∘ₛₗ f = id
⊢ Surjective ⇑(g ∘ₛₗ f)
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M : Type u_1
inst✝²⁴ : Monoid M
N : Type u_2
inst✝²³ : Monoid N
P : Type u_3
inst✝²² : Monoid P
φ : M →* N
φ' : N →* M
ψ : N →* P
χ : M →* P
A : Type u_4
inst✝²¹ : Monoid A
inst✝²⁰ : MulDistribMulAction M A
B : Type u_5
inst✝¹⁹ : Monoid B
inst✝¹⁸ : MulDistribMulAction N B
B₁ : Type u_6
inst✝¹⁷ : Monoid B₁
inst✝¹⁶ : MulDistribMulAction M B₁
C : Type u_7
inst✝¹⁵ : Monoid C
inst✝¹⁴ : MulDistribMulAction P C
A' : Type u_8
inst✝¹³ : Group A'
inst✝¹² : MulDistribMulAction M A'
B' : Type u_9
inst✝¹¹ : Group B'
inst✝¹⁰ : MulDistribMulAction N B'
R : Type u_10
inst✝⁹ : Semiring R
inst✝⁸ : MulSemiringAction M R
R' : Type u_11
inst✝⁷ : Ring R'
inst✝⁶ : MulSemiringAction M R'
S : Type u_12
inst✝⁵ : Semiring S
inst✝⁴ : MulSemiringAction N S
S' : Type u_13
inst✝³ : Ring S'
inst✝² : MulSemiringAction N S'
T : Type u_14
inst✝¹ : Semiring T
inst✝ : MulSemiringAction P T
f g : R →ₑ+*[φ] S
h : (fun m ↦ m.toFun) f = (fun m ↦ m.toFun) g
⊢ f = g

Tactic:
rcases f with ⟨⟨tF, _, _⟩, _, _⟩; rcases g with ⟨⟨tG, _, _⟩, _, _⟩
    cases tF; cases tG; congr

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

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
R : Type u_5
inst✝⁴ : Monoid R
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : MulDistribMulAction R M
inst✝ : MulDistribMulAction R N
x✝ : R
⊢ x✝ • 1 = 1

Tactic:
ext <;> exact smul_one _

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ (∀ (x y : ↥p), x = y) ↔ p = ⊥

Tactic:
Submodule.eq_bot_iff

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ (∀ (x y : ↥p), x = y) ↔ ∀ x ∈ p, x = 0
Module: Mathlib.GroupTheory.GroupAction.SubMulAction

Goal state before:
pp: R : Type u
M : Type v
inst✝¹ : Group R
inst✝ : MulAction R M
p : SubMulAction R M
x y : ↥p
⊢ (MulAction.orbitRel R ↥p) x y ↔ (Setoid.comap Subtype.val (MulAction.orbitRel R M)) x y

Tactic:
Setoid.comap_rel

Goal state after:
R : Type u
M : Type v
inst✝¹ : Group R
inst✝ : MulAction R M
p : SubMulAction R M
x y : ↥p
⊢ (MulAction.orbitRel R ↥p) x y ↔ (Setoid.comap Subtype.val (MulAction.orbitRel R M)) x y
Module: Mathlib.Algebra.Module.Submodule.RestrictScalars

Goal state before:
pp: S : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Semiring S
inst✝³ : Module S M
inst✝² : Module R M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
s : Set (Submodule R M)
⊢ restrictScalars S (sSup s) = sSup (restrictScalars S '' s)

Tactic:
simp [← toAddSubmonoid_inj, toAddSubmonoid_sSup, ← Set.image_comp]

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
S : Type u_9
N : Type u_10
N₂ : Type u_11
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Semiring R
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M
inst✝⁴ : Module R₂ M₂
inst✝³ : AddCommMonoid N
inst✝² : AddCommMonoid N₂
inst✝¹ : Module S N
inst✝ : Module S N₂
τ₁₂ : R →+* R₂
p : Submodule R M
q : Submodule R₂ M₂
pₗ : Submodule S N
qₗ : Submodule S N₂
f₁ f₂ : N →ₗ[S] N₂
h₁ : f₁ ∈ {fₗ | pₗ ≤ comap fₗ qₗ}
h₂ : f₂ ∈ {fₗ | pₗ ≤ comap fₗ qₗ}
⊢ f₁ + f₂ ∈ {fₗ | pₗ ≤ comap fₗ qₗ}

Tactic:
by
    apply le_trans _ (inf_comap_le_comap_add qₗ f₁ f₂)
    rw [le_inf_iff]
    exact ⟨h₁, h₂⟩

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

Goal state before:
pp: R : Type u
S : Type v
M : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : SMul R S
inst✝ : IsScalarTower R S M
x : R
h : IsUnit ((algebraMap R (End S M)) x)
m m' : M
H : m = x • m'
⊢ ↑h.unit⁻¹ m = m'

Tactic:
apply_fun ⇑h.unit.val using ((isUnit_iff _).mp h).injective

Goal state after:
R : Type u
S : Type v
M : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : SMul R S
inst✝ : IsScalarTower R S M
x : R
h : IsUnit ((algebraMap R (End S M)) x)
m m' : M
H : m = x • m'
⊢ ↑h.unit (↑h.unit⁻¹ m) = ↑h.unit m'
Module: Mathlib.RingTheory.NonUnitalSubring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
p : (x y : R) → x ∈ closure s → y ∈ closure s → Prop
mem_mem : ∀ (x y : R) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : R) (hx : x ∈ closure s), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : x ∈ closure s), p x 0 hx ⋯
neg_left : ∀ (x y : R) (hx : x ∈ closure s) (hy : y ∈ closure s), p x y hx hy → p (-x) y ⋯ hy
neg_right : ∀ (x y : R) (hx : x ∈ closure s) (hy : y ∈ closure s), p x y hx hy → p x (-y) hx ⋯
add_left :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y : R
hx : x ∈ closure s
hy : y ∈ closure s
⊢ p x y hx hy

Tactic:
by
  induction hy using closure_induction with
  | mem z hz => induction hx using closure_induction with
    | mem _ h => exact mem_mem _ _ h hz
    | zero => exact zero_left _ _
    | mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ _ h₁ h₂
    | add _ _ _ _ h₁ h₂ => exact add_left _ _ _ _ _ _ h₁ h₂
    | neg _ _ h => exact neg_left _ _ _ _ h
  | zero => exact zero_right x hx
  | mul _ _ _ _ h₁ h₂ => exact mul_right _ _ _ _ _ _ h₁ h₂
  | add _ _ _ _ h₁ h₂ => exact add_right _ _ _ _ _ _ h₁ h₂
  | neg _ _ h => exact neg_right _ _ _ _ h

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

Goal state before:
pp: R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
⊢ M.subsemiringClosure.toNonUnitalSubsemiring = NonUnitalSubsemiring.closure ↑M

Tactic:
refine Eq.symm (NonUnitalSubsemiring.closure_eq_of_le ?_ fun _ hx ↦ ?_)
  · simp [Submonoid.subsemiringClosure_coe]
  · simp only [Subsemiring.mem_toNonUnitalSubsemiring, subsemiringClosure_mem] at hx
    induction hx using AddSubmonoid.closure_induction <;> aesop

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

Goal state before:
pp: case cons.inr
R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : List R
HL : ∀ y ∈ hd, y ∈ s ∨ y = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : hd.prod = -L.prod
⊢ C hd.prod

pp: R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : List R
HL : ∀ y ∈ hd, y ∈ s ∨ y = -1
⊢ ∃ L, (∀ x ∈ L, x ∈ s) ∧ (hd.prod = L.prod ∨ hd.prod = -L.prod)

Tactic:
· rw [HP]
    clear HP HL hd
    induction L with
    | nil => exact hneg1
    | cons hd tl ih =>
      rw [List.prod_cons, neg_mul_eq_mul_neg]
      rw [List.forall_mem_cons] at HL'
      exact hs _ HL'.1 _ (ih HL'.2)

Goal state after:
R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : List R
HL : ∀ y ∈ hd, y ∈ s ∨ y = -1
⊢ ∃ L, (∀ x ∈ L, x ∈ s) ∧ (hd.prod = L.prod ∨ hd.prod = -L.prod)
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: case nil
R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
HL : ∀ y ∈ [], y ∈ s ∨ y = -1
⊢ ∃ L, (∀ x ∈ L, x ∈ s) ∧ ([].prod = L.prod ∨ [].prod = -L.prod)

Tactic:
exact ⟨[], List.forall_mem_nil _, Or.inl rfl⟩

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
⊢ a ~ᵤ 1 ↔ IsUnit a

Tactic:
associated_one_iff_isUnit

Goal state after:
M : Type u_1
inst✝ : Monoid M
a : M
⊢ IsUnit a ↔ IsUnit a
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonAssocRing R
G : AddSubgroup R
k : ℤ
g : R
h : g ∈ G
⊢ ↑k * g = k • g

Tactic:
zsmul_eq_mul

Goal state after:
R : Type u
inst✝ : NonAssocRing R
G : AddSubgroup R
k : ℤ
g : R
h : g ∈ G
⊢ ↑k * g = ↑k * g
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p m : Associates M
hp : Prime p
hle : m ≤ p
⊢ m = 1 ∨ m = p

Tactic:
rcases mk_surjective p with ⟨p, rfl⟩
  rcases mk_surjective m with ⟨m, rfl⟩
  simpa [mk_eq_mk_iff_associated, Associated.comm]
    using (prime_mk.1 hp).irreducible.dvd_iff.mp (mk_le_mk_iff_dvd.1 hle)

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

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_10
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
O : Submodule R M
ϕ : ↥O →ₗ[R] M'
N : Submodule R M
x : M'
y : M
yO : y ∈ O
yN : y ∈ N
h : ϕ ⟨y, yO⟩ = x
⊢ ∃ y, ∃ (yO : y ∈ O), y ∈ N ∧ ϕ ⟨y, yO⟩ = x

Tactic:
exact ⟨y, yO, yN, h⟩

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
M' : Type u_10
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
O : Submodule R M
ϕ : ↥O →ₗ[R] M'
N : Submodule R M
hNO : N ≤ O
⊢ ϕ.submoduleImage N = (ϕ ∘ₗ Submodule.inclusion hNO).range

Tactic:
by
  rw [submoduleImage, range_comp, Submodule.range_inclusion]

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a b c : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
x✝ : ↑(Ici a)
x : α
hx : x ∈ Ici a
⊢ ∃ b, IsCompl ⟨x, hx⟩ b

Tactic:
Set.Ici.isCompl_iff

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a b c : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
x✝ : ↑(Ici a)
x : α
hx : x ∈ Ici a
⊢ ∃ b, x ⊓ ↑b = a ∧ Codisjoint x ↑b
Module: Mathlib.Order.Atoms

Goal state before:
pp: A : Type u_4
B : Type u_5
inst✝³ : PartialOrder A
inst✝² : SetLike A B
inst✝¹ : IsConcreteLE A B
inst✝ : OrderBot A
K : A
⊢ (K ≠ ⊥ ∧ ∀ (b : A), b ≤ K ∧ ¬K ≤ b → b = ⊥) ↔ K ≠ ⊥ ∧ ∀ (H : A) (g : B), H ≤ K → g ∉ H → g ∈ K → H = ⊥

Tactic:
SetLike.not_le_iff_exists,

Goal state after:
A : Type u_4
B : Type u_5
inst✝³ : PartialOrder A
inst✝² : SetLike A B
inst✝¹ : IsConcreteLE A B
inst✝ : OrderBot A
K : A
⊢ (K ≠ ⊥ ∧ ∀ (b : A), (b ≤ K ∧ ∃ x ∈ K, x ∉ b) → b = ⊥) ↔ K ≠ ⊥ ∧ ∀ (H : A) (g : B), H ≤ K → g ∉ H → g ∈ K → H = ⊥
Module: Mathlib.Order.Atoms

Goal state before:
pp: A : Type u_4
B : Type u_5
inst✝³ : PartialOrder A
inst✝² : SetLike A B
inst✝¹ : IsConcreteLE A B
inst✝ : OrderTop A
K : A
⊢ (K ≠ ⊤ ∧ ∀ (b : A), K ≤ b ∧ ¬b ≤ K → b = ⊤) ↔ K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H → g ∉ K → g ∈ H → H = ⊤

Tactic:
SetLike.not_le_iff_exists,

Goal state after:
A : Type u_4
B : Type u_5
inst✝³ : PartialOrder A
inst✝² : SetLike A B
inst✝¹ : IsConcreteLE A B
inst✝ : OrderTop A
K : A
⊢ (K ≠ ⊤ ∧ ∀ (b : A), (K ≤ b ∧ ∃ x ∈ b, x ∉ K) → b = ⊤) ↔ K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H → g ∉ K → g ∈ H → H = ⊤
Module: Mathlib.Order.Atoms

Goal state before:
pp: A : Type u_4
B : Type u_5
inst✝² : PartialOrder A
inst✝¹ : SetLike A B
inst✝ : IsConcreteLE A B
K L : A
x✝ : K < L
H : A
⊢ K ≤ H → H ≤ L → (H ≠ L ∧ ¬H ≤ K ↔ H ≠ L ∧ ∃ x ∉ K, x ∈ H)

Tactic:
SetLike.not_le_iff_exists,

Goal state after:
A : Type u_4
B : Type u_5
inst✝² : PartialOrder A
inst✝¹ : SetLike A B
inst✝ : IsConcreteLE A B
K L : A
x✝ : K < L
H : A
⊢ K ≤ H → H ≤ L → ((H ≠ L ∧ ∃ x ∈ H, x ∉ K) ↔ H ≠ L ∧ ∃ x ∉ K, x ∈ H)
Module: Mathlib.Order.Atoms

Goal state before:
pp: A : Type u_4
B : Type u_5
inst✝² : PartialOrder A
inst✝¹ : SetLike A B
inst✝ : IsConcreteLE A B
K L : A
x✝ : K < L
H : A
⊢ K ≤ H → H ≤ L → (K ≠ H ∧ ¬L ≤ H ↔ H ≠ K ∧ ∃ x ∈ L, x ∉ H)

Tactic:
SetLike.not_le_iff_exists,

Goal state after:
A : Type u_4
B : Type u_5
inst✝² : PartialOrder A
inst✝¹ : SetLike A B
inst✝ : IsConcreteLE A B
K L : A
x✝ : K < L
H : A
⊢ K ≤ H → H ≤ L → ((K ≠ H ∧ ∃ x ∈ L, x ∉ H) ↔ H ≠ K ∧ ∃ x ∈ L, x ∉ H)
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
a b : α
ha : IsAtom a
hb : IsAtom b
hab : a ≠ b
⊢ Disjoint a b

Tactic:
simp [← ha.not_le_iff_disjoint, hb.le_iff, hab, ha.ne_bot]

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✝ : M
⊢ x✝ ∈ R ∙ 0 ↔ x✝ ∈ ⊥

Tactic:
simp [mem_span_singleton, eq_comm]

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : IsAtomistic α
a b : α
h : ∀ (c : α), IsAtom c → (c ≤ a ↔ c ≤ b)
⊢ (∀ (c : α), IsAtom c → c ≤ a → c ≤ b) ∧ b ≤ a

Tactic:
le_iff_atom_le_imp

Goal state after:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : IsAtomistic α
a b : α
h : ∀ (c : α), IsAtom c → (c ≤ a ↔ c ≤ b)
⊢ (∀ (c : α), IsAtom c → c ≤ a → c ≤ b) ∧ ∀ (c : α), IsAtom c → c ≤ b → c ≤ a
Module: Mathlib.LinearAlgebra.Span.Defs

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

Tactic:
simp only [Finset.coe_insert, Finset.coe_union, span_union, insert_subset_iff, SetLike.mem_coe]

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
f : M →ₛₗ[σ₁₂] M₂
s : Set M₂
⊢ span R (⇑f ⁻¹' s) ≤ comap f (span R₂ s)

Tactic:
rw [span_le, comap_coe]
  exact preimage_mono subset_span

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

Goal state before:
pp: case mp.inr.refine_1
R : Type u_8
M : Type u_9
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.IsTorsionFree R M
y : M
a b : R
hb : b • a • y = y
hy : y ≠ 0
⊢ (fun x ↦ x • y) (b * a) = (fun x ↦ x • y) 1

Tactic:
simpa only [mul_smul, one_smul]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
i : ι
s : Finset α
hs : ↑s ⊆ f '' {j | j ≠ i}
t : Finset α := s.erase ⊥
hf : InjOn f (f ⁻¹' ↑t)
h : ∀ i_1 ∈ insert i (t.preimage f hf), Disjoint (f i_1) (((insert i (t.preimage f hf)).erase i_1).sup f)
this : Finset.image f ((insert i (t.preimage f hf)).erase i) = t
⊢ Disjoint (f i) (((insert i (t.preimage f hf)).erase i).sup (id ∘ f))

Tactic:
exact h i (Finset.mem_insert_self i _)

Goal state after:
Module: Mathlib.Algebra.BigOperators.Ring.List

Goal state before:
pp: M : Type u_3
inst✝¹ : Monoid M
inst✝ : HasDistribNeg M
l : List M
⊢ (map Neg.neg l).prod = (-1) ^ l.length * l.prod

Tactic:
induction l

Goal state after:
case nil
M : Type u_3
inst✝¹ : Monoid M
inst✝ : HasDistribNeg M
⊢ (map Neg.neg []).prod = (-1) ^ [].length * [].prod

case cons
M : Type u_3
inst✝¹ : Monoid M
inst✝ : HasDistribNeg M
head✝ : M
tail✝ : List M
tail_ih✝ : (map Neg.neg tail✝).prod = (-1) ^ tail✝.length * tail✝.prod
⊢ (map Neg.neg (head✝ :: tail✝)).prod = (-1) ^ (head✝ :: tail✝).length * (head✝ :: tail✝).prod
Module: Mathlib.Data.Multiset.Antidiagonal

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
hs : s.antidiagonal = map (fun t ↦ (s - t, t)) s.powerset
⊢ map (fun x ↦ Prod.map id (cons a) x) (map (fun t ↦ (s - t, t)) s.powerset) +
      map (fun x ↦ Prod.map (cons a) id x) (map (fun t ↦ (s - t, t)) s.powerset) =
    map (fun x ↦ (a ::ₘ s - x, x)) s.powerset + map (fun x ↦ (a ::ₘ s - x, x)) (map (cons a) s.powerset)

Tactic:
map_map,

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
hs : s.antidiagonal = map (fun t ↦ (s - t, t)) s.powerset
⊢ map ((fun x ↦ Prod.map id (cons a) x) ∘ fun t ↦ (s - t, t)) s.powerset +
      map ((fun x ↦ Prod.map (cons a) id x) ∘ fun t ↦ (s - t, t)) s.powerset =
    map (fun x ↦ (a ::ₘ s - x, x)) s.powerset + map ((fun x ↦ (a ::ₘ s - x, x)) ∘ cons a) s.powerset
Module: Mathlib.Data.Multiset.Antidiagonal

Goal state before:
pp: α : Type u_1
s : Multiset α
⊢ s.antidiagonal.card = 2 ^ s.card

Tactic:
have := card_powerset s
  rwa [← antidiagonal_map_fst, card_map] at this

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
⊢ f a = g a

Tactic:
by
        have hf : f a = 0 := notMem_support_iff.1 h
        have hg : g a = 0 := by rwa [h₁, notMem_support_iff] at h
        rw [hf, hg]

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
b₁ b₂ : M
eq : single a b₁ = single a b₂
⊢ b₁ = b₂

Tactic:
by
  have : (single a b₁ : α →₀ M) a = (single a b₂ : α →₀ M) a := by rw [eq]
  rwa [single_eq_same, single_eq_same] at this

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a : α
h : f.support ⊆ {a}
x : α
⊢ f x = (single a (f a)) x

Tactic:
by_cases hx : x = a <;> simp only [hx, single_eq_same, single_eq_of_ne, Ne, not_false_iff]

Goal state after:
case neg
α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a : α
h : f.support ⊆ {a}
x : α
hx : ¬x = a
⊢ f x = 0