mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: α : Type u_1
R : Type u_5
inst✝² : Semiring R
α' : Type u_7
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
v' : α' → M'
f : α ≃ α'
l : α →₀ R
⊢ (linearCombination R v') (equivMapDomain f l) = (linearCombination R (v' ∘ ⇑f)) l

Tactic:
by
  rw [equivMapDomain_eq_mapDomain, linearCombination_mapDomain]

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

Goal state before:
pp: n : ℕ
i : Fin n
⊢ succ '' Iic i = Ioc 0 i.succ

Tactic:
refine Subset.antisymm (image_subset_iff.mpr fun j hj ↦ ⟨j.succ_pos, succ_le_succ_iff.2 hj⟩) ?_
  rintro j ⟨hj₀, hj⟩
  rcases exists_succ_eq_of_ne_zero hj₀.ne' with ⟨j, rfl⟩
  exact mem_image_of_mem _ <| succ_le_succ_iff.mp hj

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

Goal state before:
pp: M' : Type u_7
inst✝⁷ : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
b : Basis ι R M
inst✝³ : Module R M'
S : Type u_13
inst✝² : Semiring S
inst✝¹ : Module S M'
inst✝ : SMulCommClass R S M'
f : ι → M'
x : M
⊢ ((b.constr S) f) x = (b.repr x).sum fun b a ↦ a • f b

Tactic:
simp only [constr_def, LinearMap.comp_apply, lmapDomain_apply, linearCombination_apply]

Goal state after:
M' : Type u_7
inst✝⁷ : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
b : Basis ι R M
inst✝³ : Module R M'
S : Type u_13
inst✝² : Semiring S
inst✝¹ : Module S M'
inst✝ : SMulCommClass R S M'
f : ι → M'
x : M
⊢ ((mapDomain f (↑b.repr x)).sum fun i a ↦ a • id i) = (b.repr x).sum fun b a ↦ a • f b
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
s : Set α
⊢ x ∈ span R (v '' s) ↔ ∃ t, ↑t ⊆ s ∧ ∃ c, ∑ i, c i • v ↑i = x

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨t, ht, c, hx⟩ ↦ ?_⟩

Goal state after:
case refine_1
α : Type u_1
M : Type u_2
R : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
s : Set α
h : x ∈ span R (v '' s)
⊢ ∃ t, ↑t ⊆ s ∧ ∃ c, ∑ i, c i • v ↑i = x

case refine_2
α : Type u_1
M : Type u_2
R : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
s : Set α
x✝ : ∃ t, ↑t ⊆ s ∧ ∃ c, ∑ i, c i • v ↑i = x
t : Finset α
ht : ↑t ⊆ s
c : ↥t → R
hx : ∑ i, c i • v ↑i = x
⊢ x ∈ span R (v '' s)
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α → M
g : β → α
hg : InjOn g (mulSupport (f ∘ g))
⊢ ∏ᶠ (i : α) (_ : i ∈ range g), f i = ∏ᶠ (j : β), f (g j)

Tactic:
rw [← image_univ, finprod_mem_image', finprod_mem_univ]

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α → M
g : β → α
hg : InjOn g (mulSupport (f ∘ g))
⊢ InjOn g (univ ∩ mulSupport (f ∘ g))
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inr.inr
x y : ℕ∞
h : x ^ y = 1
y_0 : ¬y = 0
x_2 : 1 < x
this : (fun y ↦ x ^ y) 1 ≤ (fun y ↦ x ^ y) y
⊢ x = 1

Tactic:
simp only [epow_one, h] at this

Goal state after:
case inr.inr
x y : ℕ∞
h : x ^ y = 1
y_0 : ¬y = 0
x_2 : 1 < x
this : x ≤ 1
⊢ x = 1
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: n a b : ℕ
⊢ a + b ≡ b [MOD n] ↔ n ∣ a

Tactic:
add_modEq_right_iff

Goal state after:
n a b : ℕ
⊢ n ∣ a ↔ n ∣ a
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case succ.succ
ι : Type u_1
M : Type u_2
n n✝ : ℕ
ih : ∀ (f : Fin n → Fin (n✝ + 1)), ∑ i, ↑(f i) * (n✝ + 1) ^ ↑i < (n✝ + 1) ^ n
f : Fin (n + 1) → Fin (n✝ + 1)
⊢ (n✝ + 1) ^ n + n✝ * (n✝ + 1) ^ n = (n✝ + 1) ^ (n + 1)

Tactic:
← one_add_mul (_ : ℕ),

Goal state after:
case succ.succ
ι : Type u_1
M : Type u_2
n n✝ : ℕ
ih : ∀ (f : Fin n → Fin (n✝ + 1)), ∑ i, ↑(f i) * (n✝ + 1) ^ ↑i < (n✝ + 1) ^ n
f : Fin (n + 1) → Fin (n✝ + 1)
⊢ (1 + n✝) * (n✝ + 1) ^ n = (n✝ + 1) ^ (n + 1)
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case inl
a b c : ℕ
hmc : gcd 0 c = 1
h : c * a ≡ c * b [MOD 0]
⊢ a ≡ b [MOD 0]

Tactic:
simp only [gcd_zero_left] at hmc
    simp only [hmc, one_mul, modEq_zero_iff] at h
    subst h
    rfl

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

Goal state before:
pp: case succ.succ
ι : Type u_1
M : Type u_2
m : ℕ
ih : ∀ {n : Fin m → ℕ} (f : (i : Fin m) → Fin (n i)), ∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j) < ∏ i, n i
n✝¹ : Fin (m + 1) → ℕ
f✝ : (i : Fin (m + 1)) → Fin (n✝¹ i)
n : Fin m → ℕ
f : (i : Fin m) → Fin (n i)
n✝ : ℕ
fn : Fin (n✝ + 1)
⊢ ∏ i, n i + n✝ * ∏ j, n j = (∏ i, n i) * (n✝ + 1)

Tactic:
← one_add_mul (_ : ℕ),

Goal state after:
case succ.succ
ι : Type u_1
M : Type u_2
m : ℕ
ih : ∀ {n : Fin m → ℕ} (f : (i : Fin m) → Fin (n i)), ∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j) < ∏ i, n i
n✝¹ : Fin (m + 1) → ℕ
f✝ : (i : Fin (m + 1)) → Fin (n✝¹ i)
n : Fin m → ℕ
f : (i : Fin m) → Fin (n i)
n✝ : ℕ
fn : Fin (n✝ + 1)
⊢ (1 + n✝) * ∏ i, n i = (∏ i, n i) * (n✝ + 1)
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : ¬c = 0
⊢ ((a + b) % c + if c ≤ a % c + b % c then c else 0) = a % c + b % c

Tactic:
by
    rw [this]
    split_ifs with h
    · have h2 : (a % c + b % c) / c < 2 :=
        Nat.div_lt_of_lt_mul
          (by
            rw [mul_two]
            exact
              add_lt_add (Nat.mod_lt _ (Nat.pos_of_ne_zero hc0))
                (Nat.mod_lt _ (Nat.pos_of_ne_zero hc0)))
      have h0 : 0 < (a % c + b % c) / c := Nat.div_pos h (Nat.pos_of_ne_zero hc0)
      rw [← @add_right_cancel_iff _ _ _ (c * ((a % c + b % c) / c)), add_comm _ c, add_assoc,
        mod_add_div, le_antisymm (le_of_lt_succ h2) h0, mul_one, add_comm]
    · rw [Nat.mod_eq_of_lt (lt_of_not_ge h), add_zero]

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

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ Nat.card ↑s = hs.toFinset.card

Tactic:
by
  simp only [← Nat.card_eq_finsetCard, hs.mem_toFinset]

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

Goal state before:
pp: ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι ⊕ ι' → M
⊢ LinearIndependent R v ↔
    LinearIndependent R (v ∘ Sum.inl) ∧
      LinearIndependent R (v ∘ Sum.inr) ∧ Disjoint (span R (range (v ∘ Sum.inl))) (span R (range (v ∘ Sum.inr)))

Tactic:
rw [range_comp v, range_comp v]
  refine ⟨?_, ?_⟩
  · intro h
    refine ⟨h.comp _ Sum.inl_injective, h.comp _ Sum.inr_injective, ?_⟩
    exact h.disjoint_span_image <| isCompl_range_inl_range_inr.disjoint
  rintro ⟨hl, hr, hlr⟩
  rw [linearIndependent_iff'] at *
  intro s g hg i hi
  have :
    ((∑ i ∈ s.preimage Sum.inl Sum.inl_injective.injOn, (fun x => g x • v x) (Sum.inl i)) +
        ∑ i ∈ s.preimage Sum.inr Sum.inr_injective.injOn, (fun x => g x • v x) (Sum.inr i)) =
      0 := by
    -- Porting note: `g` must be specified.
    rw [Finset.sum_preimage' (g := fun x => g x • v x),
      Finset.sum_preimage' (g := fun x => g x • v x), ← Finset.sum_union, ← Finset.filter_or]
    · simpa only [← mem_union, range_inl_union_range_inr, mem_univ, Finset.filter_true]
    · exact Finset.disjoint_filter.2 fun x _ hx =>
        disjoint_left.1 isCompl_range_inl_range_inr.disjoint hx
  rw [← eq_neg_iff_add_eq_zero] at this
  rw [disjoint_def'] at hlr
  have A := by
    refine hlr _ (sum_mem fun i _ => ?_) _ (neg_mem <| sum_mem fun i _ => ?_) this
    · exact smul_mem _ _ (subset_span ⟨Sum.inl i, mem_range_self _, rfl⟩)
    · exact smul_mem _ _ (subset_span ⟨Sum.inr i, mem_range_self _, rfl⟩)
  rcases i with i | i
  · exact hl _ _ A i (Finset.mem_preimage.2 hi)
  · rw [this, neg_eq_zero] at A
    exact hr _ _ A i (Finset.mem_preimage.2 hi)

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
ι : Type w
v : ι → M
hv : LinearIndependent R v
⊢ lift.{v, w} #ι ≤ lift.{w, v} (Module.rank R M)

Tactic:
rw [Module.rank]

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
ι : Type w
v : ι → M
hv : LinearIndependent R v
⊢ lift.{v, w} #ι ≤ lift.{w, v} (⨆ ι, #↑↑ι)
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : LinearOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : AddRightReflectLE R
inst✝² : IsCancelAdd M
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
⊢ LinearIndependent R v ↔ ∀ (t : Finset ι) (f : ι → R), ∑ i ∈ t, f i • v i = ∑ i ∈ tᶜ, f i • v i → ∀ (i : ι), f i = 0

Tactic:
by
  rw [linearIndependent_iffₒₛ]
  refine ⟨fun h t f heq i => ?_, fun h t₁ t₂ f ht₁t₂ heq => ?_⟩
  · specialize h t tᶜ f disjoint_compl_right heq
    by_cases hi : i ∈ t
    · exact h.1 i hi
    · exact h.2 i (Finset.mem_compl.2 hi)
  · specialize h t₁ (fun i => if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) ?_
    · rw [← Finset.sum_subset ht₁t₂.le_compl_left]
      · convert! heq using 2 with i hi i hi <;> simp [hi]
      · intro i hi hi'
        simp [Finset.mem_compl.1 hi, hi']
    refine ⟨fun i hi => ?_, fun i hi => ?_⟩ <;> simpa [hi] using h i

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

Goal state before:
pp: R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
s : Set ↥f.range
li : LinearIndepOn R id s
⊢ lift.{v, v'} #↑↑⟨s, li⟩ ≤ lift.{v', v} (⨆ ι, #↑↑ι)

Tactic:
apply le_trans

Goal state after:
case a
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
s : Set ↥f.range
li : LinearIndepOn R id s
⊢ lift.{v, v'} #↑↑⟨s, li⟩ ≤ ?b

case a
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
s : Set ↥f.range
li : LinearIndepOn R id s
⊢ ?b ≤ lift.{v', v} (⨆ ι, #↑↑ι)

case b
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
s : Set ↥f.range
li : LinearIndepOn R id s
⊢ Cardinal.{max v' v}
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : Submodule R M
b : Basis ι R ↥P
x : M
| x ∈ P

Tactic:
← P.range_subtype,

Goal state after:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : Submodule R M
b : Basis ι R ↥P
x : M
| x ∈ P.subtype.range
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
⊢ Nat.card α = 0

Tactic:
by
  cases finite_or_infinite β
  · have := card_eq_zero_iff.mp h
    have := Function.isEmpty f
    exact Nat.card_of_isEmpty
  · have := Infinite.of_surjective f hf
    exact Nat.card_eq_zero_of_infinite

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

Goal state before:
pp: α : Type u_1
s t : Set α
hs : s.Finite
hsub : s ⊂ t
hle : ENat.card ↑t ≤ ENat.card ↑s
⊢ t ⊆ s

Tactic:
suffices ENat.card ↑(t \ s) ≤ 0 by
    rwa [← sdiff_eq_empty, ← Set.isEmpty_coe_sort, ← ENat.card_eq_zero_iff_empty,
      ← nonpos_iff_eq_zero]

Goal state after:
α : Type u_1
s t : Set α
hs : s.Finite
hsub : s ⊂ t
hle : ENat.card ↑t ≤ ENat.card ↑s
⊢ ENat.card ↑(t \ s) ≤ 0
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ (𝒫 s).ncard = 2 ^ s.ncard

Tactic:
have h := Cardinal.mk_powerset s

Goal state after:
α : Type u_1
s : Set α
hs : s.Finite
h : Cardinal.mk ↑(𝒫 s) = 2 ^ Cardinal.mk ↑s
⊢ (𝒫 s).ncard = 2 ^ s.ncard
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
s : Submonoid α
a : α
ha : a • ↑s = ↑s
⊢ a ∈ s

Tactic:
rw [← SetLike.mem_coe, ← ha]

Goal state after:
α : Type u_1
inst✝ : Monoid α
s : Submonoid α
a : α
ha : a • ↑s = ↑s
⊢ a ∈ a • ↑s
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
s : Submonoid α
a : α
ha : op a • ↑s = ↑s
⊢ a ∈ s

Tactic:
rw [← SetLike.mem_coe, ← ha]

Goal state after:
α : Type u_1
inst✝ : Monoid α
s : Submonoid α
a : α
ha : op a • ↑s = ↑s
⊢ a ∈ op a • ↑s
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : 1 < s.ncard
a : α
⊢ ∃ b ∈ s, b ≠ a

Tactic:
have hsf := finite_of_ncard_ne_zero (zero_lt_one.trans hs).ne.symm
  rw [ncard_eq_toFinset_card _ hsf] at hs
  simpa only [Finite.mem_toFinset] using Finset.exists_mem_ne hs a

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ LinearMap.fst R M₂ M ∘ₗ ↑(prodComm R M M₂) = LinearMap.snd R M M₂

Tactic:
by
  ext <;> simp

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ LinearMap.snd R M₂ M ∘ₗ ↑(prodComm R M M₂) = LinearMap.fst R M M₂

Tactic:
by
  ext <;> simp

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M₂ : Type w
M₃ : Type y
M₁ : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
⊢ LinearMap.fst R M₁ (M₂ × M₃) ∘ₗ ↑(prodAssoc R M₁ M₂ M₃) = LinearMap.fst R M₁ M₂ ∘ₗ LinearMap.fst R (M₁ × M₂) M₃

Tactic:
by
  ext <;> simp

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M₂ : Type w
M₃ : Type y
M₁ : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
⊢ LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ ↑(prodAssoc R M₁ M₂ M₃) = (LinearMap.snd R M₁ M₂).prodMap LinearMap.id

Tactic:
by
  ext <;> simp

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
i : ι
hf : ∀ j < i, Disjoint (f j) (f i)
⊢ disjointed f i = f i

Tactic:
disjointed_apply,

Goal state after:
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
i : ι
hf : ∀ j < i, Disjoint (f j) (f i)
⊢ f i \ (Iio i).sup f = f i
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
a b : ℕ
hab : a < b
f : ℕ → M
⊢ ∏ k ∈ Ico a b, f k = f a * ∏ k ∈ Ico (a + 1) b, f k

Tactic:
have ha : a ∉ Ico (a + 1) b := by simp
  rw [← prod_insert ha, Finset.insert_Ico_add_one_left_eq_Ico hab]

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
i : ι
hi : ¬IsMax i
⊢ disjointed f (succ i) = f (succ i) \ (partialSups f) i

Tactic:
disjointed_apply,

Goal state after:
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
i : ι
hi : ¬IsMax i
⊢ f (succ i) \ (Iio (succ i)).sup f = f (succ i) \ (partialSups f) i
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : Ring α
x y : α
⊢ span {y - x, y} = span {x, y}

Tactic:
← span_pair_sub_right,

Goal state after:
α : Type u
inst✝ : Ring α
x y : α
⊢ span {y - x - y, y} = span {x, y}
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case e'_3.h
n k : ℕ
⊢ Icc k (n + k) = map (addRightEmbedding k) (Ico 0 (n + 1))

Tactic:
rw [map_add_right_Ico, zero_add, add_right_comm, Ico_add_one_right_eq_Icc]

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: n k : ℕ
⊢ ∑ i ∈ range (n + 1), k.multichoose i = (n + k).choose k

Tactic:
cases k with
  | zero => simp [Finset.sum_range_succ']
  | succ k => grind [multichoose_eq, choose_symm_of_eq_add, sum_range_add_choose]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: R : Type u_3
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
hI : I.IsMaximal
⊢ ∀ {a : R ⧸ I}, a ≠ 0 → ∃ b, a * b = 1

Tactic:
apply exists_right_inv_of_exists_left_inv
  rintro ⟨a⟩ h
  rcases hI.exists_inv (mt eq_zero_iff_mem.2 h) with ⟨b, c, hc, abc⟩
  refine ⟨mk _ b, Quot.sound ?_⟩
  simp only [Submodule.quotientRel_def]
  rw [← eq_sub_iff_add_eq'] at abc
  rwa [abc, ← neg_mem_iff (G := R) (H := I), neg_sub] at hc

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

Goal state before:
pp: R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ IsField R ↔ ⊥.IsMaximal

Tactic:
refine ⟨fun h ↦ let := h.toSemifield; bot_isMaximal, fun hmax ↦ ?_⟩

Goal state after:
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
hmax : ⊥.IsMaximal
⊢ IsField R
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
hf : f.ker = ⊥
I : Type u_6
x : I →₀ N
⊢ (x ∈ submodule fun x ↦ f.range) → x ∈ (mapRange.linearMap f).range

Tactic:
intro hx

Goal state after:
case mpr
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
hf : f.ker = ⊥
I : Type u_6
x : I →₀ N
hx : x ∈ submodule fun x ↦ f.range
⊢ x ∈ (mapRange.linearMap f).range
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ map inl f ⊓ map inr g ≤ ⊥

Tactic:
trans map inl ⊤ ⊓ map inr ⊤

Goal state after:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ map inl f ⊓ map inr g ≤ map inl ⊤ ⊓ map inr ⊤

α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ map inl ⊤ ⊓ map inr ⊤ ≤ ⊥
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝ : SemilatticeSup β
l : Filter α
f₁ f₂ g₁ g₂ : α → β
hf : f₁ ≤ᶠ[l] f₂
hg : g₁ ≤ᶠ[l] g₂
x : α
⊢ f₁ x ≤ f₂ x → g₁ x ≤ g₂ x → (f₁ ⊔ g₁) x ≤ (f₂ ⊔ g₂) x

Tactic:
hfx

Goal state after:
α : Type u
β : Type v
inst✝ : SemilatticeSup β
l : Filter α
f₁ f₂ g₁ g₂ : α → β
hf : f₁ ≤ᶠ[l] f₂
hg : g₁ ≤ᶠ[l] g₂
x : α
hfx : f₁ x ≤ f₂ x
⊢ g₁ x ≤ g₂ x → (f₁ ⊔ g₁) x ≤ (f₂ ⊔ g₂) x
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝ : SemilatticeSup β
l : Filter α
f g h : α → β
hf : f ≤ᶠ[l] h
hg : g ≤ᶠ[l] h
x : α
⊢ f x ≤ h x → g x ≤ h x → (f ⊔ g) x ≤ h x

Tactic:
hfx

Goal state after:
α : Type u
β : Type v
inst✝ : SemilatticeSup β
l : Filter α
f g h : α → β
hf : f ≤ᶠ[l] h
hg : g ≤ᶠ[l] h
x : α
hfx : f x ≤ h x
⊢ g x ≤ h x → (f ⊔ g) x ≤ h x
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
F : Filter α
s : Set α
⊢ F ⊓ map Subtype.val ⊤ = ⊥ ↔ comap Subtype.val F = ⊥

Tactic:
← Filter.push_pull',

Goal state after:
α : Type u_1
F : Filter α
s : Set α
⊢ map Subtype.val (comap Subtype.val F ⊓ ⊤) = ⊥ ↔ comap Subtype.val F = ⊥
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: case h.right
P : ℕ → ℕ → Prop
u : ℕ → ℕ → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
n : ℕ
⊢ P n (Nat.recOn n (u 0 0) fun n v ↦ u (n + 1) v)

Tactic:
cases n <;> simp [hu']

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

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Finite G
⊢ ∃ G' x x_1, Nonempty (G ≃* G')

Tactic:
obtain ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin G

Goal state after:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
n : ℕ
e : G ≃ Fin n
⊢ ∃ G' x x_1, Nonempty (G ≃* G')
Module: Mathlib.RingTheory.Finiteness.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
⊢ N.FG ↔ ∃ S, S.Finite ∧ span R S = N

Tactic:
refine ⟨fun ⟨t, h⟩ => ⟨_, t.finite_toSet, h⟩, ?_⟩

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
⊢ (∃ S, S.Finite ∧ span R S = N) → N.FG
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
s : Set α
hs : IsCofinal s
x y : α
hy : x < y
z : α
hz : z ∈ s
hz' : y ≤ z
⊢ ∃ i ∈ s, x ∈ Iio i

Tactic:
exact ⟨z, hz, hy.trans_le hz'⟩

Goal state after:
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : SMulWithZero α β
inst✝³ : LinearOrder α
inst✝² : LinearOrder β
inst✝¹ : PosSMulMono α β
inst✝ : SMulPosMono α β
hab : 0 < a • b
ha : a < 0
⊢ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

Tactic:
refine Or.inr ⟨ha, lt_imp_lt_of_le_imp_le (fun hb ↦ ?_) hab⟩

Goal state after:
case inl
α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : SMulWithZero α β
inst✝³ : LinearOrder α
inst✝² : LinearOrder β
inst✝¹ : PosSMulMono α β
inst✝ : SMulPosMono α β
hab : 0 < a • b
ha : a < 0
hb : 0 ≤ b
⊢ a • b ≤ 0
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
sp : M → Submodule R M := fun a ↦ R ∙ a
supr_rw : ∀ (t : Finset M), ⨆ x ∈ t, sp x = ⨆ x ∈ ↑t, sp x
h : ∀ (s_1 : Set (Submodule R M)), s ≤ sSup s_1 → ∃ t, ↑t ⊆ s_1 ∧ s ≤ t.sup id
⊢ s = sSup (sp '' ↑s)

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

Goal state after:
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β
γ : Type u_3
inst✝⁹ : Zero α
inst✝⁸ : Preorder α
inst✝⁷ : Preorder β
inst✝⁶ : Preorder γ
inst✝⁵ : SMul α β
inst✝⁴ : SMul α γ
inst✝³ : Zero β
inst✝² : Zero γ
inst✝¹ : SMulPosReflectLE α β
inst✝ : SMulPosReflectLE α γ
_b : β × γ
hb : 0 < _b
_a₁ _a₂ : α
h : _a₁ • _b ≤ _a₂ • _b
h₁ : 0.1 < _b.1
⊢ _a₁ ≤ _a₂

Tactic:
exact le_of_smul_le_smul_right h.1 h₁

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s t : Set α
D : Set (Set α)
inst✝ : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
d : Set α
hD : d ∈ D
hdu✝ : d ⊆ s ∪ t
hdu : d ⊆ t ∪ s
hd₀ : d.Nonempty
hd₁ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
ha : IsLUB d a
hdst✝ : d ∩ s ∪ d ∩ t = d
hdst : d ∩ t ∪ d ∩ s = d
this :
  ∀ {α : Type u_1} {s t : Set α} {D : Set (Set α)} [inst : Preorder α],
    IsLowerSet D →
      DirSupClosedOn D s →
        DirSupClosedOn D t →
          ∀ ⦃d : Set α⦄,
            d ∈ D →
              d ⊆ s ∪ t →
                d.Nonempty →
                  DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d →
                    ∀ ⦃a : α⦄,
                      IsLUB d a →
                        d ∩ s ∪ d ∩ t = d →
                          DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (d ∩ s) ∧ IsCofinalFor (d ∩ t) (d ∩ s) → a ∈ s ∪ t
h : ¬(DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (d ∩ s) ∧ IsCofinalFor (d ∩ t) (d ∩ s))
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (d ∩ t ∪ d ∩ s)

Tactic:
rwa [hdst]

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : WellFoundedLT α
f : α → α
a : α
hf : IsNormal f
hf' : BddAbove (range fun n ↦ f^[n] a)
⊢ f (⨆ n, f^[n] a) = ⨆ n, f^[n] a

Tactic:
hf.map_iSup hf'

Goal state after:
α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : WellFoundedLT α
f : α → α
a : α
hf : IsNormal f
hf' : BddAbove (range fun n ↦ f^[n] a)
⊢ ⨆ i, f (f^[i] a) = ⨆ n, f^[n] a