mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
v : Vector α n
i j : Fin n
a : α
⊢ (v.set i a).get j = if i = j then a else v.get j

Tactic:
split_ifs

Goal state after:
case pos
α : Type u_1
n : ℕ
v : Vector α n
i j : Fin n
a : α
h✝ : i = j
⊢ (v.set i a).get j = a

case neg
α : Type u_1
n : ℕ
v : Vector α n
i j : Fin n
a : α
h✝ : ¬i = j
⊢ (v.set i a).get j = v.get j
Module: Mathlib.Order.UpperLower.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
he : IsUpperSet (range ⇑e)
a : α
⊢ ⇑e '' Ici a = Ici (e a)

Tactic:
rw [← e.preimage_Ici, image_preimage_eq_inter_range,
    inter_eq_left.2 <| he.Ici_subset (mem_range_self _)]

Goal state after:
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
D : Set (Set α)
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
h : ScottContinuousOn D f
⊢ Monotone f

Tactic:
by
  refine fun a b hab =>
    (h (hD a b hab) (insert_nonempty _ _) (directedOn_pair hab) ?_).1
      (mem_image_of_mem _ <| mem_insert _ _)
  rw [IsLUB, upperBounds_insert, upperBounds_singleton,
    inter_eq_self_of_subset_right (Ici_subset_Ici.2 hab)]
  exact isLeast_Ici

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : Mul α
a b : α
⊢ some a * some b = some (a * b)

Tactic:
by simp [mul_def]

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

Goal state before:
pp: α β : Type u
⊢ Cardinal.{u} ≤i Cardinal.{max u v}

Tactic:
refine ⟨(OrderEmbedding.ofMapLEIff lift ?_).ltEmbedding, ?_⟩ <;> intro a b

Goal state after:
case refine_1
α β : Type u
a b : Cardinal.{u}
⊢ lift.{v, u} a ≤ lift.{v, u} b ↔ a ≤ b

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
Module: Mathlib.SetTheory.Cardinal.ToNat

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

Tactic:
by
  lift c to ℕ using hc
  lift d to ℕ using hd
  norm_cast

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

Goal state before:
pp: case inl
x y : Cardinal.{u}
hle : x ≤ y
hy : y < ℵ₀
⊢ (x + y).toENatAux = x.toENatAux + y.toENatAux

Tactic:
lift x to ℕ using hle.trans_lt hy; lift y to ℕ using hy
      simp only [← Nat.cast_add, toENatAux_nat]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Monoid M
inst✝³ : Monoid N
inst✝² : MulAction M α
inst✝¹ : MulAction N α
inst✝ : SMulCommClass M N α
x y : M × N
a : α
⊢ (x * y) • a = x • y • a

Tactic:
change (x.1 * y.1) • (x.2 * y.2) • a = x.1 • x.2 • y.1 • y.2 • a

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Monoid M
inst✝³ : Monoid N
inst✝² : MulAction M α
inst✝¹ : MulAction N α
inst✝ : SMulCommClass M N α
x y : M × N
a : α
⊢ (x.1 * y.1) • (x.2 * y.2) • a = x.1 • x.2 • y.1 • y.2 • a
Module: Mathlib.Algebra.GroupWithZero.Action.Prod

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : AddMonoid α
inst✝² : DistribMulAction M α
inst✝¹ : DistribMulAction N α
inst✝ : SMulCommClass M N α
mn : M × N
⊢ mn • 0 = 0

Tactic:
change mn.1 • mn.2 • 0 = (0 : α)

Goal state after:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : AddMonoid α
inst✝² : DistribMulAction M α
inst✝¹ : DistribMulAction N α
inst✝ : SMulCommClass M N α
mn : M × N
⊢ mn.1 • mn.2 • 0 = 0
Module: Mathlib.Algebra.Module.Submodule.LinearMap

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
ι : Type u_9
inst✝¹³ : Semiring R
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring 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₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₃] M₃
M₂' : Type u_10
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
p : M₂' →ₗ[R₂] M₂
hp : Injective ⇑p
h : ∀ (c : M), f c ∈ range ⇑p
r : R
c : M
⊢ p (Exists.choose ⋯) = p (σ₁₂ r • Exists.choose ⋯)

Tactic:
simp_rw [map_smul, (h _).choose_spec, 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 α
x : α × α
s : Set (α × α)
⊢ (⨆ a ∈ s, a.1) ⊔ ⨆ a ∈ s, a.2 = ⨆ a ∈ s, a.1 ⊔ a.2

Tactic:
iSup_sup_eq

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

Goal state before:
pp: K : Type u_9
V : Type u_10
V₂ : Type u_11
inst✝⁴ : Semifield K
inst✝³ : AddCommMonoid V
inst✝² : Module K V
inst✝¹ : AddCommMonoid V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
p : Submodule K V₂
a : K
⊢ comap (a • f) p = ⨅ (_ : a ≠ 0), comap f p

Tactic:
by_cases h : a = 0 <;> simp [h, comap_smul]

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

Goal state before:
pp: M : Type u_2
inst✝ : Mul M
ι : Sort u_3
S : ι → Subsemigroup M
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : M
⊢ x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i

Tactic:
refine ⟨?_, fun ⟨i, hi⟩ ↦ le_iSup S i hi⟩

Goal state after:
M : Type u_2
inst✝ : Mul M
ι : Sort u_3
S : ι → Subsemigroup M
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : M
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i
Module: Mathlib.Algebra.Group.Subsemigroup.Membership

Goal state before:
pp: case refine_2
M : Type u_2
inst✝ : Mul M
ι : Sort u_3
S : ι → Subsemigroup M
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x✝ : M
hx : x✝ ∈ closure (⋃ i, ↑(S i))
x y : M
hx✝ : x ∈ closure (⋃ i, ↑(S i))
hy✝ : y ∈ closure (⋃ i, ↑(S i))
i : ι
hi : x ∈ S i
j : ι
hj : y ∈ S j
⊢ ∃ i, x * y ∈ S i

Tactic:
obtain ⟨k, hik, hjk⟩ := hS i j

Goal state after:
case refine_2
M : Type u_2
inst✝ : Mul M
ι : Sort u_3
S : ι → Subsemigroup M
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x✝ : M
hx : x✝ ∈ closure (⋃ i, ↑(S i))
x y : M
hx✝ : x ∈ closure (⋃ i, ↑(S i))
hy✝ : y ∈ closure (⋃ i, ↑(S i))
i : ι
hi : x ∈ S i
j : ι
hj : y ∈ S j
k : ι
hik : S i ≤ S k
hjk : S j ≤ S k
⊢ ∃ i, x * y ∈ S i
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ ↑(Int.negSucc n) * (x✝¹ * x✝) = ↑(Int.negSucc n) * x✝¹ * x✝

Tactic:
Int.cast_negSucc,

Goal state after:
M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ -↑(n + 1) * (x✝¹ * x✝) = -↑(n + 1) * x✝¹ * x✝
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic

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

Tactic:
refine ⟨?_, fun ⟨i, hi⟩ ↦ le_iSup S i hi⟩

Goal state after:
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
ι : Sort u_2
hι : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : R
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i
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
    rw [H]
    simpa using Module.End.isUnit_apply_inv_apply_of_isUnit h (x • m')

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

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

Tactic:
| mem _ _ hx hy =>

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

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

Tactic:
induction h using AddSubgroup.closure_induction with

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

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

Tactic:
refine ⟨?_, fun ⟨i, hi⟩ ↦ le_iSup S i hi⟩

Goal state after:
R : Type u
inst✝ : NonUnitalNonAssocRing R
ι : Sort u_1
hι : Nonempty ι
S : ι → NonUnitalSubring R
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : R
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : Semiring R
s : Set R
x : R
⊢ (∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x) → x ∈ closure s

Tactic:
· rintro ⟨L, HL1, rfl⟩
    exact
      list_sum_mem fun r hr =>
        let ⟨t, ht1, ht2⟩ := List.mem_map.1 hr
        ht2 ▸ list_prod_mem _ fun y hy => subset_closure <| HL1 t ht1 y hy

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

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

Tactic:
refine ⟨?_, fun ⟨i, hi⟩ ↦ le_iSup S i hi⟩

Goal state after:
R : Type u
inst✝ : NonAssocSemiring R
ι : Sort u_1
hι : Nonempty ι
S : ι → Subsemiring R
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : R
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: case mul.mem
R : Type u
inst✝ : NonAssocRing R
s : Set R
x x✝¹ y✝¹ x✝ y✝ : R
hx : x✝ ∈ ↑(Submonoid.closure s)
hy : y✝ ∈ ↑(Submonoid.closure s)
⊢ x✝ * y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)

Tactic:
| mem _ _ hx hy =>

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

Goal state before:
pp: R : Type u
inst✝ : NonAssocRing R
s : Set R
x : R
h : x ∈ AddSubgroup.closure ↑(Submonoid.closure s)
⊢ x ∈ closure s

Tactic:
induction h using AddSubgroup.closure_induction with

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

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

Tactic:
refine ⟨?_, fun ⟨i, hi⟩ ↦ le_iSup S i hi⟩

Goal state after:
R : Type u
inst✝ : NonAssocRing R
ι : Sort u_1
hι : Nonempty ι
S : ι → Subring R
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : R
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
⊢ Associates.mk a ∈ (Associates M₀)⁰ ↔ a ∈ M₀⁰

Tactic:
rw [mem_nonZeroDivisors_iff_right, mem_nonZeroDivisors_iff_right]
  contrapose!
  constructor
  · rintro ⟨⟨x⟩, hx₁, hx₂⟩
    refine ⟨x, ?_, ?_⟩
    · rwa [← Associates.mk_eq_zero, ← Associates.mk_mul_mk, ← Associates.quot_mk_eq_mk]
    · rwa [← Associates.mk_ne_zero, ← Associates.quot_mk_eq_mk]
  · refine fun ⟨b, hb₁, hb₂⟩ ↦ ⟨Associates.mk b, ?_, by rwa [Associates.mk_ne_zero]⟩
    rw [Associates.mk_mul_mk, hb₁, Associates.mk_zero]

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

Goal state before:
pp: case closed_under_smul
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
inst✝ : SMulCommClass S R M
r : S
⊢ ∀ ⦃r_1 : S⦄ ⦃n : M⦄, r_1 ∈ {r} → n ∈ N → r_1 • n ∈ r • N

pp: case le
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
inst✝ : SMulCommClass S R M
r : S
⊢ r • N ≤ {r} • N

Tactic:
· rintro _ m rfl hm; exact ⟨m, hm, rfl⟩

Goal state after:
case le
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
inst✝ : SMulCommClass S R M
r : S
⊢ r • N ≤ {r} • N
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝ : Lattice α
h : ∀ (x y z : α), x ⊓ z ⊔ y ⊓ z = (x ⊓ z ⊔ y) ⊓ z
x✝ y z : α
xz : x✝ ≤ z
⊢ (x✝ ⊔ y) ⊓ z ≤ x✝ ⊔ y ⊓ z

Tactic:
by rw [← inf_eq_left.2 xz, h]

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
p p' : Submodule R M
h : x ∈ p ⊔ p'
⊢ ∃ y ∈ p, ∃ z ∈ p', y + z = x

Tactic:
by
    rw [← span_eq p, ← span_eq p', ← span_union] at h
    refine span_induction ?_ ?_ ?_ ?_ h
    · rintro y (h | h)
      · exact ⟨y, h, 0, by simp, by simp⟩
      · exact ⟨0, by simp, y, h, by simp⟩
    · exact ⟨0, by simp, 0, by simp⟩
    · rintro _ _ - - ⟨y₁, hy₁, z₁, hz₁, rfl⟩ ⟨y₂, hy₂, z₂, hz₂, rfl⟩
      exact ⟨_, add_mem hy₁ hy₂, _, add_mem hz₁ hz₂, by
        rw [add_assoc, add_assoc, ← add_assoc y₂, ← add_assoc z₁, add_comm y₂]⟩
    · rintro a - _ ⟨y, hy, z, hz, rfl⟩
      exact ⟨_, smul_mem _ a hy, _, smul_mem _ a hz, by simp [smul_add]⟩

Goal state after:
Module: Mathlib.Order.Atoms

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

Tactic:
refine (Set.OrdConnected.apply_covBy_apply_iff (OrderEmbedding.subtype fun c => a ≤ c) ?_).symm

Goal state after:
α : Type u_2
inst✝ : PartialOrder α
a : α
b : ↑(Ici a)
⊢ (range ⇑(OrderEmbedding.subtype fun c ↦ a ≤ c)).OrdConnected
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : IsAtomistic α
b : α
⊢ b = ⊥ ∨ ∃ a, IsAtom a ∧ a ≤ b

Tactic:
rcases isLUB_atoms b with ⟨s, hsb, hs⟩

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

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : IsAtomistic α
b : α
⊢ IsLUB {a | IsAtom a ∧ a ≤ b} b

Tactic:
rcases isLUB_atoms b with ⟨s, hsb, hs⟩

Goal state after:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : IsAtomistic α
b : α
s : Set α
hsb : IsLUB s b
hs : ∀ a ∈ s, IsAtom a
⊢ IsLUB {a | IsAtom a ∧ a ≤ b} b
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α✝
α : Type u_4
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
⊢ b ≤ sSup {a | IsAtom a ∧ a ≤ b}

Tactic:
have : (⨅ c : α, ⨆ x, b ⊓ cond x c (cᶜ)) = b := by simp [iSup_bool_eq]

Goal state after:
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α✝
α : Type u_4
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
this : (⨅ c, ⨆ x, b ⊓ bif x then c else cᶜ) = b
⊢ b ≤ sSup {a | IsAtom a ∧ a ≤ b}
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 ⊥ ↔ ⊤ ≤ ⊥

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

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case mpr.inr
α : Type u_1
inst✝ : CompleteLattice α
a c : α
hab : a ≠ c
h : Disjoint a c
⊢ Disjoint c (sSup ({a, c} \ {c}))

Tactic:
convert! h.symm using 1

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
a c : α
hab : a ≠ c
h : Disjoint a c
⊢ sSup ({a, c} \ {c}) = a
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_5
inst✝ : CompleteLattice α
f : Fin 3 → α
⊢ ⨆ i, f i = f 0 ⊔ f 1 ⊔ f 2

Tactic:
by
  suffices ⨆ i ∈ Finset.univ, f i = f 0 ⊔ f 1 ⊔ f 2 by simp [← this]
  rw [← Finset.sup_eq_iSup, show (Finset.univ : Finset (Fin 3)) = {0, 1, 2} from rfl]
  simp [sup_assoc]

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝ : CommMonoid M
s : Finset ι
f : ι → κ → M
⊢ (mulSupport fun x ↦ ∏ i ∈ s, f i x) ⊆ ⋃ i ∈ s, mulSupport (f i)

Tactic:
by
  simp only [mulSupport_subset_iff', Set.mem_iUnion, not_exists, notMem_mulSupport]
  exact fun x ↦ prod_eq_one

Goal state after:
Module: Mathlib.Algebra.Notation.Indicator

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝ : One M
s t : Set α
f : α → M
x : α
⊢ (if x ∈ s then if x ∈ t then f x else 1 else 1) = if x ∈ s ∩ t then f x else 1

Tactic:
split_ifs

Goal state after:
case pos
α : Type u_1
M : Type u_3
inst✝ : One M
s t : Set α
f : α → M
x : α
h✝² : x ∈ s
h✝¹ : x ∈ t
h✝ : x ∈ s ∩ t
⊢ f x = f x

case neg
α : Type u_1
M : Type u_3
inst✝ : One M
s t : Set α
f : α → M
x : α
h✝² : x ∈ s
h✝¹ : x ∈ t
h✝ : ¬x ∈ s ∩ t
⊢ f x = 1

case pos
α : Type u_1
M : Type u_3
inst✝ : One M
s t : Set α
f : α → M
x : α
h✝² : x ∈ s
h✝¹ : ¬x ∈ t
h✝ : x ∈ s ∩ t
⊢ 1 = f x

case neg
α : Type u_1
M : Type u_3
inst✝ : One M
s t : Set α
f : α → M
x : α
h✝² : x ∈ s
h✝¹ : ¬x ∈ t
h✝ : ¬x ∈ s ∩ t
⊢ 1 = 1

case pos
α : Type u_1
M : Type u_3
inst✝ : One M
s t : Set α
f : α → M
x : α
h✝¹ : ¬x ∈ s
h✝ : x ∈ s ∩ t
⊢ 1 = f x

case neg
α : Type u_1
M : Type u_3
inst✝ : One M
s t : Set α
f : α → M
x : α
h✝¹ : ¬x ∈ s
h✝ : ¬x ∈ s ∩ t
⊢ 1 = 1
Module: Mathlib.Algebra.Algebra.Tower

Goal state before:
pp: R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra S A
inst✝⁴ : Algebra S B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
r : R
⊢ (↑↑↑f).toFun ((algebraMap S A) ((algebraMap R S) r)) = (algebraMap S B) ((algebraMap R S) r)

Tactic:
exact f.commutes (algebraMap R S r)

Goal state after:
Module: Mathlib.Algebra.Notation.Indicator

Goal state before:
pp: α : Type u_1
M : Type u_3
N : Type u_4
inst✝¹ : One M
inst✝ : One N
s : Set α
f : α → M
g : M → N
hg : g 1 = 1
x✝ : α
⊢ (if x✝ ∈ s then (g ∘ f) x✝ else 1) = (g ∘ s.mulIndicator f) x✝

Tactic:
split_ifs

Goal state after:
case pos
α : Type u_1
M : Type u_3
N : Type u_4
inst✝¹ : One M
inst✝ : One N
s : Set α
f : α → M
g : M → N
hg : g 1 = 1
x✝ : α
h✝ : x✝ ∈ s
⊢ (g ∘ f) x✝ = (g ∘ s.mulIndicator f) x✝

case neg
α : Type u_1
M : Type u_3
N : Type u_4
inst✝¹ : One M
inst✝ : One N
s : Set α
f : α → M
g : M → N
hg : g 1 = 1
x✝ : α
h✝ : ¬x✝ ∈ s
⊢ 1 = (g ∘ s.mulIndicator f) x✝
Module: Mathlib.Algebra.Algebra.Tower

Goal state before:
pp: R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra S A
inst✝⁴ : Algebra S B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S B
f : A ≃ₐ[S] B
r : R
⊢ f.toRingEquiv.toFun ((algebraMap S A) ((algebraMap R S) r)) = (algebraMap S B) ((algebraMap R S) r)

Tactic:
exact f.commutes (algebraMap R S r)

Goal state after:
Module: Mathlib.Algebra.Notation.Indicator

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝ : One M
t : Set α
s : Set M
⊢ (if 1 ∈ s then univ else ∅) ∈ {univ, ∅}

Tactic:
split_ifs

Goal state after:
case pos
α : Type u_1
M : Type u_3
inst✝ : One M
t : Set α
s : Set M
h✝ : 1 ∈ s
⊢ univ ∈ {univ, ∅}

case neg
α : Type u_1
M : Type u_3
inst✝ : One M
t : Set α
s : Set M
h✝ : ¬1 ∈ s
⊢ ∅ ∈ {univ, ∅}
Module: Mathlib.Algebra.Notation.Indicator

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝² : One M
U : Set α
s : Set M
a : M
inst✝¹ : Decidable (a ∈ s)
inst✝ : Decidable (1 ∈ s)
⊢ U.ite (if a ∈ s then univ else ∅) (if 1 ∈ s then univ else ∅) = (if a ∈ s then U else ∅) ∪ if 1 ∈ s then Uᶜ else ∅

Tactic:
split_ifs

Goal state after:
case pos
α : Type u_1
M : Type u_3
inst✝² : One M
U : Set α
s : Set M
a : M
inst✝¹ : Decidable (a ∈ s)
inst✝ : Decidable (1 ∈ s)
h✝¹ : a ∈ s
h✝ : 1 ∈ s
⊢ U.ite univ univ = U ∪ Uᶜ

case neg
α : Type u_1
M : Type u_3
inst✝² : One M
U : Set α
s : Set M
a : M
inst✝¹ : Decidable (a ∈ s)
inst✝ : Decidable (1 ∈ s)
h✝¹ : a ∈ s
h✝ : ¬1 ∈ s
⊢ U.ite univ ∅ = U ∪ ∅

case pos
α : Type u_1
M : Type u_3
inst✝² : One M
U : Set α
s : Set M
a : M
inst✝¹ : Decidable (a ∈ s)
inst✝ : Decidable (1 ∈ s)
h✝¹ : ¬a ∈ s
h✝ : 1 ∈ s
⊢ U.ite ∅ univ = ∅ ∪ Uᶜ

case neg
α : Type u_1
M : Type u_3
inst✝² : One M
U : Set α
s : Set M
a : M
inst✝¹ : Decidable (a ∈ s)
inst✝ : Decidable (1 ∈ s)
h✝¹ : ¬a ∈ s
h✝ : ¬1 ∈ s
⊢ U.ite ∅ ∅ = ∅ ∪ ∅
Module: Mathlib.Algebra.Notation.Indicator

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝ : One M
U : Set α
s : Set M
a : M
⊢ ((if a ∈ s then U else ∅) ∪ if 1 ∈ s then Uᶜ else ∅) ∈ {univ, U, Uᶜ, ∅}

Tactic:
split_ifs

Goal state after:
case pos
α : Type u_1
M : Type u_3
inst✝ : One M
U : Set α
s : Set M
a : M
h✝¹ : a ∈ s
h✝ : 1 ∈ s
⊢ U ∪ Uᶜ ∈ {univ, U, Uᶜ, ∅}

case neg
α : Type u_1
M : Type u_3
inst✝ : One M
U : Set α
s : Set M
a : M
h✝¹ : a ∈ s
h✝ : ¬1 ∈ s
⊢ U ∪ ∅ ∈ {univ, U, Uᶜ, ∅}

case pos
α : Type u_1
M : Type u_3
inst✝ : One M
U : Set α
s : Set M
a : M
h✝¹ : ¬a ∈ s
h✝ : 1 ∈ s
⊢ ∅ ∪ Uᶜ ∈ {univ, U, Uᶜ, ∅}

case neg
α : Type u_1
M : Type u_3
inst✝ : One M
U : Set α
s : Set M
a : M
h✝¹ : ¬a ∈ s
h✝ : ¬1 ∈ s
⊢ ∅ ∪ ∅ ∈ {univ, U, Uᶜ, ∅}
Module: Mathlib.Algebra.Algebra.Tower

Goal state before:
pp: case refine_1
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
hs : span R s = ⊤
t : Set A
x✝ : A
hp : x✝ ∈ restrictScalars R (span S t)
s0 : S
y : A
hy : y ∈ t
⊢ 0 • y ∈ span R (s • t)

Tactic:
rw [zero_smul]; apply zero_mem

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

Goal state before:
pp: I : Type u_7
inst✝² : DecidableEq I
M : I → Type u_8
inst✝¹ : (i : I) → CommMonoid (M i)
inst✝ : Fintype I
f : (i : I) → M i
⊢ ∏ i, Pi.mulSingle i (f i) = f

Tactic:
by
  ext a
  simp

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

Goal state before:
pp: α : Type u_1
s : Multiset α
x : Multiset α × Multiset α
l : List α
⊢ x ∈ antidiagonal ⟦l⟧ ↔ x.1 + x.2 = ⟦l⟧

Tactic:
by
    dsimp only [quot_mk_to_coe, antidiagonal_coe]
    refine ⟨fun h => revzip_powersetAux h, fun h ↦ ?_⟩
    have _ := Classical.decEq α
    simp only [revzip_powersetAux_lemma l revzip_powersetAux, h.symm, mem_coe,
      List.mem_map, mem_powersetAux]
    obtain ⟨x₁, x₂⟩ := x
    exact ⟨x₁, le_add_right _ _, by rw [add_tsub_cancel_left x₁ x₂]⟩

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
K : Type u_3
M : Type u_4
M₂ : Type u_5
V : Type u_6
S : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x : M
p p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s✝ t : Set M
s : Submodule R M
⊢ sSup ((fun x ↦ R ∙ x) '' ↑s) = s

Tactic:
by
        rw [sSup_eq_iSup, iSup_image, ← span_eq_iSup_of_singleton_spans, span_eq]

Goal state after: