mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Control.Applicative

Goal state before:
pp: F : Type u → Type v
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α β γ σ : Type u
f : α → β → γ
g : σ → β
x : F α
y : F σ
⊢ f <$> x <*> g <$> y = ((fun x ↦ x ∘ g) ∘ f) <$> x <*> y

Tactic:
simp [functor_norm, Function.comp_def]

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
s : Finset ι
p : ι → Prop
inst✝ : DecidablePred p
f : (x : ι) → p x → M
g : (x : ι) → ¬p x → M
⊢ (∏ x ∈ s, if hx : p x then f x hx else g x hx) = (∏ x, f ↑x ⋯) * ∏ x, g ↑x ⋯

Tactic:
simp [prod_apply_dite _ _ fun x => x]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p : α → Prop
f : α → σ → σ × β
x : List α
px : x.length = n
c : σ
res : σ × List β := List.mapAccumr f x c
⊢ res.snd.length = n

Tactic:
by simp [*, res]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p : α → Prop
f : α → β → σ → σ × φ
x : List α
px : x.length = n
y : List β
py : y.length = n
c : σ
res : σ × List φ := List.mapAccumr₂ f x y c
⊢ res.snd.length = n

Tactic:
by simp [*, res]

Goal state after:
Module: Mathlib.Data.Fintype.Sum

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
⊢ image (fun i ↦ b ↑i) univ ⊆ (image b univ).erase k

Tactic:
image_subset_iff

Goal state after:
case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
⊢ ∀ x ∈ univ, b ↑x ∈ (image b univ).erase k
Module: Mathlib.Data.Fintype.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
⊢ image (fun i ↦ b ↑i) univ = (image b univ).erase k

Tactic:
by
  apply subset_antisymm
  · rw [image_subset_iff]
    intro i _
    apply mem_erase_of_ne_of_mem i.2 (mem_image_of_mem _ (mem_univ _))
  · intro i hi
    rw [mem_image]
    rcases mem_image.1 (erase_subset _ _ hi) with ⟨a, _, ha⟩
    subst ha
    exact ⟨⟨a, ne_of_mem_erase hi⟩, mem_univ _, rfl⟩

Goal state after:
Module: Mathlib.Data.Fintype.BigOperators

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝¹ : Fintype α
inst✝ : CommMonoid M
f : α → M
a b : α
h₁ : a ≠ b
h₂ : ∀ (x : α), x ≠ a ∧ x ≠ b → f x = 1
⊢ ∏ x, f x = f a * f b

Tactic:
apply Finset.prod_eq_mul a b h₁ fun x _ hx => h₂ x hx

Goal state after:
case ha
α : Type u_1
M : Type u_4
inst✝¹ : Fintype α
inst✝ : CommMonoid M
f : α → M
a b : α
h₁ : a ≠ b
h₂ : ∀ (x : α), x ≠ a ∧ x ≠ b → f x = 1
⊢ a ∉ Finset.univ → f a = 1

case hb
α : Type u_1
M : Type u_4
inst✝¹ : Fintype α
inst✝ : CommMonoid M
f : α → M
a b : α
h₁ : a ≠ b
h₂ : ∀ (x : α), x ≠ a ∧ x ≠ b → f x = 1
⊢ b ∉ Finset.univ → f b = 1
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case cons
n : ℕ
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
n✝ : ℕ
x✝ : α
w✝ : Vector α n✝
ih : Vector.traverse (Comp.mk ∘ Functor.map f ∘ g) w✝ = Comp.mk (Vector.traverse f <$> Vector.traverse g w✝)
⊢ cons <$> (Comp.mk ∘ Functor.map f ∘ g) x✝ <*> Comp.mk (Vector.traverse f <$> Vector.traverse g w✝) =
    Comp.mk (Vector.traverse f <$> Vector.traverse g (x✝ ::ᵥ w✝))

Tactic:
simp [functor_norm, Function.comp_def]

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
b : β
h : ∀ (b : β), ∃ x, x ∈ Set.range ⇑f ∧ ¬s x b ∨ x ∉ Set.range ⇑f ∧ s x b
x : β
IH : ∀ (y : β), s y x → ∃ a, f a = y
y : β
hy : y ∈ Set.range ⇑f
hs : ¬s y x
⊢ ∃ a, f a = x

Tactic:
obtain (rfl | h) := (trichotomous y x).resolve_left hs
    · exact hy
    · obtain ⟨z, rfl⟩ := hy
      exact f.mem_range_of_rel h

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
hc : ↑c ⊆ {y | IsExtremePt x f y}
y : α
hy : y ∈ bot x f
hy' : y < cSup c
⊢ ∃ z ∈ c, ¬f z ≤ y

Tactic:
by
      by_contra! h
      apply lt_irrefl y (lt_of_lt_of_le hy' ?_)
      apply cSup_le
      intro z hz
      exact le_trans (le_map z) (h z hz)

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
c : Chain (Part α)
a b : α
ha : some a ∈ c
hb : some b ∈ c
⊢ a = b

Tactic:
obtain ⟨i, ha⟩ := ha; replace ha := ha.symm
  obtain ⟨j, hb⟩ := hb; replace hb := hb.symm
  rw [eq_some_iff] at ha hb
  rcases le_total i j with hij | hji
  · have := c.monotone hij _ ha; apply mem_unique this hb
  · have := c.monotone hji _ hb; apply Eq.symm; apply mem_unique this ha

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : OmegaCompletePartialOrder α
inst✝² : OmegaCompletePartialOrder β
inst✝¹ : OmegaCompletePartialOrder γ
inst✝ : OmegaCompletePartialOrder δ
⊢ Function.Injective fun f ↦ f.toFun

Tactic:
by rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩ h; congr

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

Goal state before:
pp: a b c : Cardinal.{u_1}
h : b ≤ c
⊢ a ^ b ≤ max (a ^ c) 1

Tactic:
by_cases ha : a = 0

Goal state after:
case pos
a b c : Cardinal.{u_1}
h : b ≤ c
ha : a = 0
⊢ a ^ b ≤ max (a ^ c) 1

case neg
a b c : Cardinal.{u_1}
h : b ≤ c
ha : ¬a = 0
⊢ a ^ b ≤ max (a ^ c) 1
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i < g i
x✝ : prod g ≤ sum f
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
i : ι
⊢ #(Quotient.out (g i)) ≠ 0

Tactic:
rw [mk_out]

Goal state after:
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i < g i
x✝ : prod g ≤ sum f
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
i : ι
⊢ g i ≠ 0
Module: Mathlib.Algebra.Ring.CompTypeclasses

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
inst✝² : Semiring R₁
inst✝¹ : Semiring R₂
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
inst✝ : RingHomInvPair σ σ'
x : R₁
⊢ (σ'.comp σ) x = x

Tactic:
comp_eq

Goal state after:
R₁ : Type u_1
R₂ : Type u_2
inst✝² : Semiring R₁
inst✝¹ : Semiring R₂
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
inst✝ : RingHomInvPair σ σ'
x : R₁
⊢ (RingHom.id R₁) x = x
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case refine_1
a b : Cardinal.{u_1}
h : a * b < ℵ₀
⊢ a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀

Tactic:
by_cases ha : a = 0

Goal state after:
case pos
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : a = 0
⊢ a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀

case neg
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : ¬a = 0
⊢ a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
ι : Type v
f : ι → Set α
⊢ (sum fun i ↦ #↑(f i)) = sum fun i ↦ lift.{v, u} #↑(f i)

Tactic:
rw [← lift_sum, lift_id'.{_, u}]

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

Goal state before:
pp: case neg
α : Type u
s : Set α
a : α
h : a ∉ s
⊢ #↑(insert a s) ≤ #↑s + 1

Tactic:
· rw [mk_insert h]

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

Goal state before:
pp: case inr
α : Type u
A B : Set α
hfin : A.Finite
hlt : A ⊂ B
hinf : Infinite ↑B
⊢ #↑A < #↑B

Tactic:
exact (lt_aleph0_iff_subtype_finite.mpr hfin).trans_le <| Cardinal.aleph0_le_mk_iff.mpr hinf

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

Goal state before:
pp: α : Type u
S T : Set α
h : T ⊆ S
⊢ #↑(S \ T ∪ T) = #↑S

Tactic:
by rw [sdiff_union_of_subset h]

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

Goal state before:
pp: α : Type u
β : Type v
f : α ≃ β
s : Set β
⊢ s ⊆ univ

Tactic:
exact fun _ _ ↦ ⟨⟩

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

Goal state before:
pp: α : Type u
⊢ #α = 2 ↔ ∃ x y, x ≠ y ∧ {x, y} = univ

Tactic:
by
  classical
  simp only [← @Nat.cast_two Cardinal, mk_eq_nat_iff_finset, Finset.card_eq_two]
  constructor
  · rintro ⟨t, ht, x, y, hne, rfl⟩
    exact ⟨x, y, hne, by simpa using ht⟩
  · rintro ⟨x, y, hne, h⟩
    exact ⟨{x, y}, by simpa using h, x, y, hne, rfl⟩

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

Goal state before:
pp: α : Type u_1
h : 3 ≤ #α
x y : α
this : ↑3 ≤ #α
⊢ ↑2 < #α

Tactic:
rwa [← natCast_add_one_le_iff, ← Nat.cast_add_one]

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Free

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹⁰ : Semiring R
inst✝⁹ : Semiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsTorsionFree R M
inst✝⁴ : Module S R
inst✝³ : IsTorsionFree S R
inst✝² : IsScalarTower S R R
inst✝¹ : SMulCommClass S R R
inst✝ : IsScalarTower S R M
s : S
hs : IsRegular s
x y : M
hxy : (fun x ↦ s • x) x = (fun x ↦ s • x) y
⊢ x = y

Tactic:
refine (?_ : IsRegular (s • 1 : R)).isSMulRegular (by simpa using hxy)
    exact ⟨fun x y hxy ↦ hs.isSMulRegular <| by simpa using hxy,
      fun x y hxy ↦ hs.isSMulRegular <| by simpa using hxy⟩

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

Goal state before:
pp: case inr
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✝ : SupSet α
x✝ : CompleteLattice β
s : Set α
hs : s.Nonempty
⊢ ⊥ = sSup ((fun x ↦ ⊥) '' s)

Tactic:
rw [hs.image_const, sSup_singleton]

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
ι : Type u_9
f : M →ₛₗ[σ₁₂] M₂
s : Finset ι
p : ι → Submodule R₂ M₂
⊢ comap f (s.inf p) = s.inf fun i ↦ comap f (p i)

Tactic:
simp [Finset.inf_eq_iInf]

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

Goal state before:
pp: R✝ : Type u_1
A : Type u_2
M : Type u_3
R : Type u_4
inst✝² : CommRing R
inst✝¹ : Semiring A
inst✝ : Algebra R A
z : ℕ
⊢ (algebraMap R A) ↑↑z = ↑z

Tactic:
simp only [Int.cast_natCast, map_natCast]

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

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

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

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

Goal state before:
pp: case mp.mem
R : Type u_1
inst✝ : Semiring R
s : Set R
x✝ x : R
hx : x ∈ ↑(Submonoid.closure s)
⊢ ∃ t, (∀ y ∈ t, y ∈ s) ∧ t.prod = x

Tactic:
induction hx using Submonoid.closure_induction with

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NonAssocRing T
g : S →+* T
f : R →+* S
⊢ Subring.map g f.range = (g.comp f).range

Tactic:
by
  simpa only [range_eq_map] using (⊤ : Subring R).map_map g f

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

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

Tactic:
induction hx using Submonoid.closure_induction with

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
p q : M
hq : Irreducible q
left✝ : p ≠ 0
x : M
hx : ¬IsUnit x
hx' : q = p * x
⊢ IsUnit p

Tactic:
exact ((irreducible_iff.1 hq).right hx').resolve_right hx

Goal state after:
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 τ₁₂
⊢ range 0 = ⊥

Tactic:
simpa only [range_eq_map] using Submodule.map_zero _

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Prod

Goal state before:
pp: ι : Type u_7
κ : Type u_8
α : Type u_9
β : Type u_10
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
s : Finset ι
t : Finset κ
ht : t.Nonempty
f : ι → α
g : κ → β
i : α × β
a : ι
ha : a ∈ s
⊢ (s ×ˢ t).sup (Prod.map f g) ≤ i ↔ (s.sup f, t.sup g) ≤ i

Tactic:
obtain ⟨b, hb⟩ := ht

Goal state after:
ι : Type u_7
κ : Type u_8
α : Type u_9
β : Type u_10
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
s : Finset ι
t : Finset κ
f : ι → α
g : κ → β
i : α × β
a : ι
ha : a ∈ s
b : κ
hb : b ∈ t
⊢ (s ×ˢ t).sup (Prod.map f g) ≤ i ↔ (s.sup f, t.sup g) ≤ i
Module: Mathlib.Data.Finset.Lattice.Prod

Goal state before:
pp: ι : Type u_7
κ : Type u_8
α : Type u_9
β : Type u_10
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s : Finset ι
t : Finset κ
ht : t.Nonempty
f : ι → α
g : κ → β
i : α × β
a : ι
ha : a ∈ s
⊢ (s.sup' ⋯ f, t.sup' ht g) ≤ i ↔ (s ×ˢ t).sup' ⋯ (Prod.map f g) ≤ i

Tactic:
obtain ⟨b, hb⟩ := ht

Goal state after:
ι : Type u_7
κ : Type u_8
α : Type u_9
β : Type u_10
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s : Finset ι
t : Finset κ
f : ι → α
g : κ → β
i : α × β
a : ι
ha : a ∈ s
b : κ
hb : b ∈ t
⊢ (s.sup' ⋯ f, t.sup' ⋯ g) ≤ i ↔ (s ×ˢ t).sup' ⋯ (Prod.map f g) ≤ i
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a b c : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
hb : a ≤ b
hc : b ≤ c
⊢ ∃ b', b ⊓ b' = a ∧ b ⊔ b' = c

Tactic:
obtain ⟨d, hdisjoint, hcodisjoint⟩ := exists_isCompl b
  refine ⟨(d ⊔ a) ⊓ c, ?_, ?_⟩
  · simpa [← inf_assoc, ← inf_sup_assoc_of_le _ hb, hdisjoint.eq_bot] using hb.trans hc
  · simp [← sup_inf_assoc_of_le _ hc, ← sup_assoc, hcodisjoint.eq_top]

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: ι : Sort u_1
F : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s t : Set α
a b : α
⊢ ∀ ⦃x y : Set α⦄, x ⊆ y → SupClosed y → {a | ∃ t, ∃ (ht : t.Nonempty), ↑t ⊆ x ∧ t.sup' ht id = a} ⊆ y

Tactic:
rintro s₁ s₂ hs h₂ _ ⟨t, ht, hts, rfl⟩; exact h₂.finsetSup'_mem ht fun i hi ↦ hs <| hts hi

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

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set M
x✝ : M
hx✝ : x✝ ∈ span R S
x : M
hx : x ∈ S
⊢ ∃ T, ↑T ⊆ S ∧ x ∈ span R ↑T

Tactic:
refine ⟨{x}, ?_, ?_⟩
    · rwa [Finset.coe_singleton, Set.singleton_subset_iff]
    · rw [Finset.coe_singleton]
      exact Submodule.mem_span_singleton_self x

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

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_8
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
k : ι
⊢ update v j (v j + r • v i) k ∈ span R (range v)

Tactic:
obtain rfl | hjk := eq_or_ne j k

Goal state after:
case refine_1.inl
R : Type u_1
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_8
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
⊢ update v j (v j + r • v i) j ∈ span R (range v)

case refine_1.inr
R : Type u_1
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_8
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
k : ι
hjk : j ≠ k
⊢ update v j (v j + r • v i) k ∈ span R (range v)
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_8
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
k : ι
⊢ v k ∈ span R (range (update v j (v j + r • v i)))

Tactic:
obtain rfl | hjk := eq_or_ne j k

Goal state after:
case refine_2.inl
R : Type u_1
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_8
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
⊢ v j ∈ span R (range (update v j (v j + r • v i)))

case refine_2.inr
R : Type u_1
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_8
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
k : ι
hjk : j ≠ k
⊢ v k ∈ span R (range (update v j (v j + r • v i)))
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case mp
α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : IsCompactElement k
s : Set α
hs : s.Nonempty
hs' : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
⊢ k ≤ sSup s → ∃ x ∈ s, k ≤ x

Tactic:
h_le

Goal state after:
case mp
α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : IsCompactElement k
s : Set α
hs : s.Nonempty
hs' : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
h_le : k ≤ sSup s
⊢ ∃ x ∈ s, k ≤ x
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
s : Set α
⊢ IsCoatom s ↔ ∃ x, s = {x}ᶜ

Tactic:
by
  rw [isCompl_compl.isCoatom_iff_isAtom, isAtom_iff]
  simp_rw [@eq_comm _ s, compl_eq_comm]

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

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
u : α
hs : s.Nonempty
hs' : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hu : IsLUB s u
⊢ k ≤ u → ∃ x ∈ s, k ≤ x

Tactic:
h_le

Goal state after:
case mpr
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
u : α
hs : s.Nonempty
hs' : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hu : IsLUB s u
h_le : k ≤ u
⊢ ∃ x ∈ s, k ≤ x
Module: Mathlib.Order.CompactlyGenerated.Basic

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

Tactic:
isCompactElement_iff_le_of_directed_sSup_le

Goal state after:
α : Type u_2
inst✝ : CompleteLattice α
k : α
⊢ (∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x) ↔
    ∀ (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case mpr.inl
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
j k : ι
hij : k ≠ j
huniv : ∀ (k_1 : ι), k_1 = k ∨ k_1 = j
h : Disjoint (t k) (t j)
i : ι
hi : i ≠ k
⊢ t i = t j

Tactic:
(huniv i).resolve_left hi

Goal state after:
case mpr.inl
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
j k : ι
hij : k ≠ j
huniv : ∀ (k_1 : ι), k_1 = k ∨ k_1 = j
h : Disjoint (t k) (t j)
i : ι
hi : i ≠ k
⊢ t j = t j
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : IsCompactElement k
ι : Type u_3
f : ι → α
h : k ≤ ⨆ i, f i
⊢ ∃ s, k ≤ ⨆ i ∈ s, f i

Tactic:
isCompactElement_iff_le_of_directed_sSup_le

Goal state after:
α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
ι : Type u_3
f : ι → α
h : k ≤ ⨆ i, f i
⊢ ∃ s, k ≤ ⨆ i ∈ s, f i
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_3
inst✝ : CompleteLattice α
k : α
hk : IsCompactElement k
s : Set α
hemp : s.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hbelow : ∀ x ∈ s, x < k
⊢ sSup s < k

Tactic:
isCompactElement_iff_le_of_directed_sSup_le

Goal state after:
α : Type u_3
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hemp : s.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hbelow : ∀ x ∈ s, x < k
⊢ sSup s < k
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ x ∈ s, IsCompactElement (f x)
⊢ IsCompactElement (s.sup f)

Tactic:
isCompactElement_iff_le_of_directed_sSup_le

Goal state after:
α : Type u_3
β : Type u_4
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ x ∈ s, ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → f x ≤ sSup s → ∃ x_1 ∈ s, f x ≤ x_1
⊢ ∀ (s_1 : Set α), s_1.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s_1 → s.sup f ≤ sSup s_1 → ∃ x ∈ s_1, s.sup f ≤ x
Module: Mathlib.Algebra.Algebra.Tower

Goal state before:
pp: 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
x : S
hx : x ∈ s
⊢ x • y ∈ s • t

Tactic:
by exact ⟨x, hx, y, hy, rfl⟩

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
s : Set ι
a : α
hs : ∀ t ⊆ s, t.Finite → Disjoint (⨆ i ∈ t, f i) a
⊢ Disjoint (⨆ i ∈ s, f i) a

Tactic:
simp_rw [disjoint_iff, iSup_subtype', ← sSup_range, inf_comm, inf_sSup_eq_iSup_inf_sup_finset,
    iSup_eq_bot]

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
s : Set ι
a : α
hs : ∀ t ⊆ s, t.Finite → Disjoint (⨆ i ∈ t, f i) a
⊢ ∀ (i : Finset α), (↑i ⊆ range fun x ↦ f ↑x) → a ⊓ i.sup id = ⊥
Module: Mathlib.Algebra.BigOperators.Pi

Goal state before:
pp: ι✝ : Type u_1
κ : Type u_2
M✝ : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
M : ι → Type u_8
inst✝¹ : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst✝ : CommMonoid M'
φ : (i : ι) → M i →* M'
i : ι
m : M i
φ' : (i : ι) → M i → M' := fun i ↦ ⇑(φ i)
⊢ ∏ x, (φ x) (mulSingle i m x) = (φ i) m

Tactic:
conv =>
      enter [1, 2, j]
      rw [show φ j = φ' j from rfl, Pi.apply_mulSingle φ' (fun i ↦ map_one (φ i))]

Goal state after:
ι✝ : Type u_1
κ : Type u_2
M✝ : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
M : ι → Type u_8
inst✝¹ : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst✝ : CommMonoid M'
φ : (i : ι) → M i →* M'
i : ι
m : M i
φ' : (i : ι) → M i → M' := fun i ↦ ⇑(φ i)
⊢ Finset.univ.prod (mulSingle i (φ' i m)) = (φ i) m
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case refine_2.refine_2
α : 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 : a ⊓ (b ⊔ sSup s) = ⊥
⊢ a ≤ b ⊔ sSup s

Tactic:
refine (le_sSup ?_).trans le_sup_right

Goal state after:
case refine_2.refine_2
α : 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 : a ⊓ (b ⊔ sSup s) = ⊥
⊢ a ∈ s
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝⁴ : CommRing S
inst✝³ : PartialOrder S
inst✝² : IsOrderedRing S
inst✝¹ : Ring R
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a : R
⊢ abv (-a) = abv a

Tactic:
by_cases ha : a = 0

Goal state after:
case pos
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing S
inst✝³ : PartialOrder S
inst✝² : IsOrderedRing S
inst✝¹ : Ring R
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a : R
ha : a = 0
⊢ abv (-a) = abv a

case neg
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing S
inst✝³ : PartialOrder S
inst✝² : IsOrderedRing S
inst✝¹ : Ring R
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a : R
ha : ¬a = 0
⊢ abv (-a) = abv a