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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a b : α ⊕ β
⊢ a < b ↔ a ≤ b ∧ ¬b ≤ a

Tactic:
by
      refine ⟨fun hab => ⟨hab.mono (fun _ _ => le_of_lt) fun _ _ => le_of_lt, ?_⟩, ?_⟩
      · rintro (⟨hba⟩ | ⟨hba⟩)
        · exact hba.not_gt (inl_lt_inl_iff.1 hab)
        · exact hba.not_gt (inr_lt_inr_iff.1 hab)
      · rintro ⟨⟨hab⟩ | ⟨hab⟩, hba⟩
        · exact LiftRel.inl (hab.lt_of_not_ge fun h => hba <| LiftRel.inl h)
        · exact LiftRel.inr (hab.lt_of_not_ge fun h => hba <| LiftRel.inr h)

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
H : IsWellOrder α r
a : α
b : β
h : s b ((ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) a)
⊢ b ∈ Set.range ⇑(ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯)

Tactic:
obtain ⟨m, hm, hm'⟩ := H.wf.has_min { a | ¬s _ b } ⟨_, asymm h⟩
    use m
    obtain lt | rfl | gt := trichotomous_of s b (collapseF f m)
    · refine (collapseF_not_lt f m (fun c h ↦ ?_) lt).elim
      by_contra hn
      exact hm' _ hn h
    · rfl
    · exact (hm gt).elim

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
a b : α
hab : a ≤ b
⊢ Set.range ⇑(pair a b hab) = {a, b}

Tactic:
ext; exact Nat.or_exists_add_one.symm.trans (by aesop)

Goal state after:
Module: Mathlib.Order.FixedPoints

Goal state before:
pp: case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h : ωScottContinuous ⇑f
a : α
h_a : f a ≤ a
⊢ ⨆ n, (⇑f)^[n] ⊥ ≤ a

Tactic:
exact ωSup_iterate_le_prefixedPoint ⟨f, h.map_ωSup_of_orderHom⟩ ⊥ bot_le h_a bot_le

Goal state after:
Module: Mathlib.Order.Zorn

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : Preorder α
a : α
ih : ∀ c ⊆ Ici a, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub, ∀ z ∈ c, z ≤ ub
x : α
hax : a ≤ x
m : α
hxm : x ≤ m
ham : (fun x ↦ x ∈ Ici a) m
hm : ∀ ⦃y : α⦄, (fun x ↦ x ∈ Ici a) y → m ≤ y → y ≤ m
⊢ ∃ m, x ≤ m ∧ IsMax m

pp: case refine_1
α : Type u_1
inst✝ : Preorder α
a : α
ih : ∀ c ⊆ Ici a, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub, ∀ z ∈ c, z ≤ ub
x : α
hax : a ≤ x
c : Set α
hca : c ⊆ Ici a
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
y : α
hy : y ∈ c
⊢ ∃ ub ∈ Ici a, ∀ z ∈ c, z ≤ ub

Tactic:
· exact ⟨m, hxm, fun z hmz => hm (ham.trans hmz) hmz⟩

Goal state after:
case refine_1
α : Type u_1
inst✝ : Preorder α
a : α
ih : ∀ c ⊆ Ici a, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub, ∀ z ∈ c, z ≤ ub
x : α
hax : a ≤ x
c : Set α
hca : c ⊆ Ici a
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
y : α
hy : y ∈ c
⊢ ∃ ub ∈ Ici a, ∀ z ∈ c, z ≤ ub
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : 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 : ℕ
y : γ
b : β
hb₀ : b ∈ f (c i)
hb₁ : y ∈ g (c i) b
⊢ b ∈ ωSup (c.map f)

Tactic:
· apply le_ωSup (c.map f) i _ hb₀

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

Goal state before:
pp: α β : Type u
c : Cardinal.{u}
f : α → β
hf : ∀ (b : β), #↑(f ⁻¹' {b}) ≤ c
⊢ #α ≤ #β * c

Tactic:
simpa only [← mk_congr (@Equiv.sigmaFiberEquiv α β f), mk_sigma, ← sum_const'] using!
    sum_le_sum _ _ hf

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : MonoidWithZero R
inst✝¹ : Zero M
inst✝ : MulActionWithZero R M
⊢ (¬∃ x y, x ≠ y) ↔ Subsingleton M

Tactic:
subsingleton_iff

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : MonoidWithZero R
inst✝¹ : Zero M
inst✝ : MulActionWithZero R M
⊢ (¬∃ x y, x ≠ y) ↔ ∀ (x y : M), x = y
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
n : ℕ
⊢ #α = ↑n ↔ Nonempty (α ≃ Fin n)

Tactic:
rw [← lift_mk_fin, ← lift_uzero #α, lift_mk_eq']

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

Goal state before:
pp: case mpr
α : Type u
n : ℕ
t : Finset α
ht : ∀ (x : α), x ∈ t
hn : Fintype.card α = n
⊢ ∃ t, ↑t = univ ∧ t.card = n

Tactic:
exact ⟨t, eq_univ_iff_forall.2 ht, hn⟩

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S✝ : Subsemigroup M
f : M →ₙ* N
S : Subsemigroup N
a✝ b✝ : M
ha : a✝ ∈ ⇑f ⁻¹' ↑S
hb : b✝ ∈ ⇑f ⁻¹' ↑S
⊢ f a✝ * f b✝ ∈ S

Tactic:
exact mul_mem ha hb

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

Goal state before:
pp: M : Type u_1
inst✝¹ : Mul M
N : Type u_5
inst✝ : Mul N
f : M →ₙ* N
⊢ ↑f.srange = ↑⊤ ↔ Set.range ⇑f = Set.univ

Tactic:
by rw [coe_srange, coe_top]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : NonUnitalNonAssocSemiring R
F : Type u_1
inst✝² : FunLike F R S
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalRingHomClass F R S
f : F
⊢ ↑(srange f) = ↑⊤ ↔ Set.range ⇑f = Set.univ

Tactic:
by rw [coe_srange, coe_top]

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 (↑h.unit⁻¹ m) = ↑h.unit m'

Tactic:
H

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⁻¹ (x • m')) = ↑h.unit m'
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' = ↑h.unit (↑h.unit⁻¹ m)

Tactic:
H

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 m' = ↑h.unit (↑h.unit⁻¹ (x • m'))
Module: Mathlib.Algebra.Algebra.Basic

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : CommSemiring F
inst✝¹ : Semiring E
inst✝ : Algebra F E
b : F →ₗ[F] E
hb : Surjective ⇑b
x y : F
hy : b y = b 1 * b 1
⊢ (algebraMap F E) (x * y) = b x

Tactic:
obtain ⟨z, hz⟩ := hb 1

Goal state after:
F : Type u_1
E : Type u_2
inst✝² : CommSemiring F
inst✝¹ : Semiring E
inst✝ : Algebra F E
b : F →ₗ[F] E
hb : Surjective ⇑b
x y : F
hy : b y = b 1 * b 1
z : F
hz : b z = 1
⊢ (algebraMap F E) (x * y) = b x
Module: Mathlib.Algebra.Prime.Lemmas

Goal state before:
pp: case refine_1
M : Type u_1
N : Type u_2
inst✝⁵ : CommMonoidWithZero M
inst✝⁴ : CommMonoidWithZero N
F : Type u_3
G : Type u_4
inst✝³ : FunLike F M N
inst✝² : MonoidWithZeroHomClass F M N
inst✝¹ : FunLike G N M
inst✝ : MulHomClass G N M
f : F
g : G
p : M
hinv : ∀ (a : M), g (f a) = a
hp : Prime (f p)
a b : M
h✝ : p ∣ a * b
h : f p ∣ f a
⊢ p ∣ a

Tactic:
convert! ← map_dvd g h <;> apply hinv

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

Goal state before:
pp: case refine_2
M : Type u_1
N : Type u_2
inst✝⁵ : CommMonoidWithZero M
inst✝⁴ : CommMonoidWithZero N
F : Type u_3
G : Type u_4
inst✝³ : FunLike F M N
inst✝² : MonoidWithZeroHomClass F M N
inst✝¹ : FunLike G N M
inst✝ : MulHomClass G N M
f : F
g : G
p : M
hinv : ∀ (a : M), g (f a) = a
hp : Prime (f p)
a b : M
h✝ : p ∣ a * b
h : f p ∣ f b
⊢ p ∣ b

Tactic:
convert! ← map_dvd g h <;> apply hinv

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

Goal state before:
pp: M₀ : Type u_2
inst✝¹ : MonoidWithZero M₀
inst✝ : NoZeroDivisors M₀
S : Submonoid M₀
hS : 0 ∉ S
hx : 0 ∈ S
⊢ False

Tactic:
exact hS hx

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
p q : M
h : p ~ᵤ q
hp : Prime p
u : Mˣ
hu : p * ↑u = q
⊢ ∀ (a b : M), q ∣ a * b → q ∣ a ∨ q ∣ b

Tactic:
rw [← hu]

Goal state after:
M : Type u_1
inst✝ : CommMonoidWithZero M
p q : M
h : p ~ᵤ q
hp : Prime p
u : Mˣ
hu : p * ↑u = q
⊢ ∀ (a b : M), p * ↑u ∣ a * b → p * ↑u ∣ a ∨ p * ↑u ∣ b
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case mpr
M : Type u_1
inst✝ : CommMonoidWithZero M
a : M
⊢ (∀ ⦃a_1 b : M⦄, a = a_1 * b → IsUnit a_1 ∨ IsUnit b) → ∀ (a_2 a_3 : M), a_2 * a_3 ~ᵤ a → IsUnit a_2 ∨ IsUnit a_3

Tactic:
rintro h x y ⟨u, rfl⟩
    simpa using h (mul_assoc _ _ _)

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

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

Tactic:
← range_le_bot_iff,

Goal state after:
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 = ⊥ ↔ f.range ≤ ⊥
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
inst✝ : SMulCommClass S R M
s : Set S
N : Submodule R M
⊢ {p | ∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p} = Set.Ici (⨆ a ∈ s, a • N)

Tactic:
simp_rw [← Set.Ici_def, iSup_le_iff, @forall_comm M]

Goal state after:
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
inst✝ : SMulCommClass S R M
s : Set S
N : Submodule R M
⊢ {p | ∀ ⦃r : S⦄, r ∈ s → ∀ a ∈ N, r • a ∈ p} = {x | ∀ i ∈ s, i • N ≤ x}
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝ : DistribLattice α
x✝ y z : α
xz : x✝ ≤ z
⊢ x✝ ⊓ z ⊔ y ⊓ z ≤ x✝ ⊔ y ⊓ z

Tactic:
inf_eq_left.2 xz

Goal state after:
α : Type u_1
inst✝ : DistribLattice α
x✝ y z : α
xz : x✝ ≤ z
⊢ x✝ ⊔ y ⊓ z ≤ x✝ ⊔ y ⊓ z
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
s : Set M
⊢ p ⊔ span R s = span R (↑p ∪ s)

Tactic:
Submodule.span_union,

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
s : Set M
⊢ p ⊔ span R s = span R ↑p ⊔ span R s
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
s : Set M
⊢ span R s ⊔ p = span R (s ∪ ↑p)

Tactic:
Submodule.span_union,

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
s : Set M
⊢ span R s ⊔ p = span R s ⊔ span R ↑p
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝ : Frame α
f : ι → α
a : α
ha : IsAtom a
⊢ a ≤ iSup f ↔ ∃ i, a ≤ f i

Tactic:
refine ⟨?_, fun ⟨i, hi⟩ => le_trans hi (le_iSup _ _)⟩
  change (a ≤ ⨆ i, f i) → _
  refine fun h => of_not_not fun ha' => ?_
  push Not at ha'
  have ha'' : Disjoint a (⨆ i, f i) :=
    disjoint_iSup_iff.2 fun i => fun x hxa hxf => le_bot_iff.2 <| of_not_not fun hx =>
      have hxa : x < a := (le_iff_eq_or_lt.1 hxa).resolve_left (by rintro rfl; exact ha' _ hxf)
      hx (ha.2 _ hxa)
  obtain rfl := le_bot_iff.1 (ha'' le_rfl h)
  exact ha.1 rfl

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝² : PartialOrder α✝
α : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : IsStronglyAtomic α
⊢ IsStronglyCoatomic αᵒᵈ

Tactic:
by
  rwa [isStronglyCoatomic_dual_iff_is_stronglyAtomic]

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
ι : Sort u_9
p : ι → Submodule R M
m : M
⊢ (∀ (b : Submodule R M), (∀ (i : ι), p i ≤ b) → R ∙ m ≤ b) ↔ ∀ (N : Submodule R M), (∀ (i : ι), p i ≤ N) → m ∈ N

Tactic:
simp only [span_singleton_le_iff_mem]

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : DistribLattice α
s : Set α
hs : s.Finite
⊢ (supClosure (infClosure s)).Finite

Tactic:
exact hs.infClosure.supClosure

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : DistribLattice α
s : Set α
hs : s.Finite
⊢ (_root_.latticeClosure s).Finite

Tactic:
by
  rw [← supClosure_infClosure]; exact hs.infClosure.supClosure

Goal state after:
Module: Mathlib.Order.Interval.Set.OrderIso

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
a b : α
⊢ ⇑e '' Icc a b = Icc (e a) (e b)

Tactic:
rw [e.image_eq_preimage_symm, e.symm.preimage_Icc, e.symm_symm]

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsUpperModularLattice α
inst✝ : IsAtomistic α
a b : α
hab : a < b
⊢ ∃ x, a ⋖ x ∧ x ≤ b

Tactic:
obtain ⟨s, hsb, h⟩ := isLUB_atoms b
    refine by_contra fun hcon ↦ hab.not_ge <| (isLUB_le_iff hsb).2 fun x hx ↦ ?_
    simp_rw [not_exists, and_comm (b := _ ≤ _), not_and] at hcon
    specialize hcon (x ⊔ a) (sup_le (hsb.1 hx) hab.le)
    obtain (hbot | h_inf) := (h x hx).bot_covBy.eq_or_eq (c := x ⊓ a) (by simp) (by simp)
    · exact False.elim <| hcon <|
        (hbot ▸ IsUpperModularLattice.covBy_sup_of_inf_covBy) (h x hx).bot_covBy
    rwa [inf_eq_left] at h_inf

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 w✝¹ : ι
w✝ : π w✝¹
left✝ : IsAtom w✝
hs : Function.update ⊥ w✝¹ w✝ ≤ s
⊢ Function.eval i (Function.update ⊥ w✝¹ w✝) ≤ s i

Tactic:
exact hs i

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
ι : Sort u_5
ι' : Sort u_6
t : ι → α
f : ι' → ι
ht : iSupIndep (t ∘ f)
hf : Surjective f
i' : ι'
⊢ Disjoint (t (f i')) (⨆ x, ⨆ (_ : f x ≠ f i'), t (f x))

Tactic:
exact (ht i').mono_right (biSup_mono fun j' hij => mt (congr_arg f) hij)

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₀
ih : ∀ {t : Set ι}, Disjoint (↑s₀) t → Disjoint (⨆ i ∈ s₀, f i) (⨆ i ∈ t, f i)
t : Set ι
hst : Disjoint (↑(insert j s₀)) t
hjt : j ∉ t
⊢ Disjoint (⨆ i ∈ insert j s₀, f i) (⨆ i ∈ t, f i)

Tactic:
replace hst : Disjoint ↑s₀ (insert j t) := by aesop

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₀
ih : ∀ {t : Set ι}, Disjoint (↑s₀) t → Disjoint (⨆ i ∈ s₀, f i) (⨆ i ∈ t, f i)
t : Set ι
hjt : j ∉ t
hst : Disjoint (↑s₀) (insert j t)
⊢ Disjoint (⨆ i ∈ insert j s₀, f i) (⨆ i ∈ t, f i)
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: case mp
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
x y : M
⊢ ((∃ a, a • y = x) ∧ ∃ a, a • x = y) → ∃ z, z • x = y

Tactic:
rintro ⟨⟨a, rfl⟩, b, hb⟩

Goal state after:
case mp
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
⊢ ∃ z, z • a • y = y
Module: Mathlib.Data.Multiset.Sections

Goal state before:
pp: α : Type u_1
s : Multiset (Multiset α)
⊢ ∀ {a : Multiset α}, a ∈ s.Sections ↔ Rel (fun s a ↦ a ∈ s) s a

Tactic:
induction s using Multiset.induction_on with

Goal state after:
Module: Mathlib.Data.Multiset.Antidiagonal

Goal state before:
pp: α : Type u_1
s t : Multiset α
⊢ (s + t).antidiagonal = s.antidiagonal.bind fun p ↦ map (fun q ↦ (p.1 + q.1, p.2 + q.2)) t.antidiagonal

Tactic:
induction s using Multiset.induction_on with

Goal state after:
Module: Mathlib.Data.Multiset.Antidiagonal

Goal state before:
pp: α : Type u_1
s : Multiset α
⊢ map Prod.swap s.antidiagonal = s.antidiagonal

Tactic:
induction s using Multiset.induction_on with

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

Goal state before:
pp: R : Type u_4
inst✝ : CommSemiring R
s✝ : Multiset (Multiset R)
a : Multiset R
s : Multiset (Multiset R)
ih : (map sum s).prod = (map prod s.Sections).sum
⊢ (map sum (a ::ₘ s)).prod = (map prod (a ::ₘ s).Sections).sum

Tactic:
simp [ih, map_bind, sum_map_mul_left, sum_map_mul_right]

Goal state after:
Module: Mathlib.Data.Multiset.Antidiagonal

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
⊢ s.antidiagonal = map (fun t ↦ (s - t, t)) s.powerset

Tactic:
induction s using Multiset.induction_on with

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

Goal state after:
α : 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 ∨ x = a
⊢ Disjoint x (sSup ((s ∪ {a}) \ {x}))
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: case insert.e_a.e_f
ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
κ : ι → Type u_5
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∏ a ∈ s, ∑ b ∈ t a, f a b = ∑ p ∈ s.pi t, ∏ x ∈ s.attach, f (↑x) (p ↑x ⋯)
h₁ : ∀ x ∈ t a, ∀ y ∈ t a, x ≠ y → Disjoint (image (Pi.cons s a x) (s.pi t)) (image (Pi.cons s a y) (s.pi t))
b : κ a
x✝¹ : b ∈ t a
h₂ : ∀ p₁ ∈ s.pi t, ∀ p₂ ∈ s.pi t, Pi.cons s a b p₁ = Pi.cons s a b p₂ → p₁ = p₂
g : (a : ι) → a ∈ s → κ a
x✝ : g ∈ s.pi t
v : ι
hv : v ∈ s
⊢ g ↑⟨v, hv⟩ ⋯ = Pi.cons s a b g ↑⟨v, hv⟩ ⋯

Tactic:
exact (Pi.cons_ne (by rintro rfl; exact ha hv)).symm

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}
⊢ IsAtom x ∧ x ≤ c

Tactic:
rw [Set.mem_union, Set.mem_singleton_iff] at hx

Goal state after:
α : 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 ∨ x = a
⊢ IsAtom x ∧ x ≤ c
Module: Mathlib.Data.Multiset.Find

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
hp : {x | x ∈ s ∧ p x}.Subsingleton
⊢ find? p s hp = some a ↔ a ∈ s ∧ p a

Tactic:
induction s using Multiset.induction_on with

Goal state after:
Module: Mathlib.Data.Multiset.Find

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
hp : {x | x ∈ s ∧ p x}.Subsingleton
⊢ find? p s hp = none ↔ ∀ (a : α), a ∈ s → ¬p a

Tactic:
induction s using Multiset.induction_on with

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

Goal state before:
pp: case mp
α : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
g : α →₀ N
⊢ (∃ y, mapRange e he₀ y = g) → ∀ (i : α), ∃ y, e y = g i

pp: case mpr
α : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
g : α →₀ N
⊢ (∀ (i : α), ∃ y, e y = g i) → ∃ y, mapRange e he₀ y = g

Tactic:
· grind

Goal state after:
case mpr
α : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
g : α →₀ N
⊢ (∀ (i : α), ∃ y, e y = g i) → ∃ y, mapRange e he₀ y = g
Module: Mathlib.Data.Finsupp.Defs

Goal state before:
pp: α : Type u_1
M : Type u_4
N : Type u_5
O : Type u_6
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero O
D : DecidableEq α
f : M → N → O
hf : f 0 0 = 0
g₁ : α →₀ M
g₂ : α →₀ N
⊢ (zipWith f hf g₁ g₂).support ⊆ g₁.support ∪ g₂.support

Tactic:
by
  convert! support_onFinset_subset

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

Goal state before:
pp: ι : Type u_1
F : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
G : Type u_6
H : Type u_7
inst✝¹ : AddZeroClass M
inst✝ : AddZeroClass N
f✝ : M → N
g₁ g₂ : ι →₀ M
f : ι ↪ F
v w : ι →₀ M
⊢ embDomain f (v + w) = embDomain f v + embDomain f w

Tactic:
ext b
    by_cases h : b ∈ Set.range f
    · rcases h with ⟨a, rfl⟩
      simp
    · simp only [coe_add, Pi.add_apply, embDomain_of_notMem_range _ _ _ h, add_zero]

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
β : Type u_3
inst✝ : CommMonoid β
f : ι → κ
s : Finset κ
hf : Set.InjOn f (f ⁻¹' ↑s)
g : κ → β
hg : ∀ x ∈ s, x ∉ Set.range f → g x = 1
⊢ ∏ x ∈ s.preimage f hf, g (f x) = ∏ x ∈ s, g x

Tactic:
prod_preimage',

Goal state after:
ι : Type u_1
κ : Type u_2
β : Type u_3
inst✝ : CommMonoid β
f : ι → κ
s : Finset κ
hf : Set.InjOn f (f ⁻¹' ↑s)
g : κ → β
hg : ∀ x ∈ s, x ∉ Set.range f → g x = 1
⊢ ∏ x ∈ s with x ∈ Set.range f, g x = ∏ x ∈ s, g x
Module: Mathlib.Data.Finsupp.Single

Goal state before:
pp: case mpr
α : Type u_1
M : Type u_5
inst✝ : Zero M
a₁ a₂ : α
b₁ b₂ : M
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0 → single a₁ b₁ = single a₂ b₂

Tactic:
· grind

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : AddCommMonoid M
k l m n : ι
u v : M
hu : u ≠ 0
hv : v ≠ 0
⊢ Pi.single k u + Pi.single l v = Pi.single m u + Pi.single n v ↔
    k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n

Tactic:
exact Pi.single_add_single_eq_single_add_single hu hv

Goal state after: