mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Congruence.Basic

Goal state before:
pp: R : Type u_3
inst✝¹ : Add R
inst✝ : Mul R
⊢ Subsingleton (RingCon R) ↔ Subsingleton R

Tactic:
by
  simp_rw [← not_nontrivial_iff_subsingleton, nontrivial_iff]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' p'' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ comap f q
⊢ p ≤ (q.mkQ ∘ₛₗ f).ker

Tactic:
simpa [ker_comp] using h

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
J : Set ι
I : Finset ι
hIJ : Codisjoint (↑I) J
b : (i : ι) → φ i
hb : ∀ i ∈ J, b i = 0
i : ι
⊢ ∑ c ∈ I, Pi.single c (b c) i = b i

Tactic:
← Pi.single_eq_same i (b i)

Goal state after:
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
J : Set ι
I : Finset ι
hIJ : Codisjoint (↑I) J
b : (i : ι) → φ i
hb : ∀ i ∈ J, b i = 0
i : ι
⊢ ∑ c ∈ I, Pi.single c (b c) i = Pi.single i (b i) i
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
M : Type v
ι : Type x
inst✝⁹ : Semiring R
φ : ι → Type i
inst✝⁸ : (i : ι) → AddCommMonoid (φ i)
inst✝⁷ : (i : ι) → Module R (φ i)
inst✝⁶ : DecidableEq ι
S : Type u_1
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Fintype ι
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
f : (i : ι) → φ i →ₗ[R] M
i : ι
x : φ i
⊢ ((lsum R φ S) f) (Pi.single i x) = (f i) x

Tactic:
by
  simp_rw [lsum_apply, sum_apply, comp_apply, proj_apply, apply_single, Fintype.sum_pi_single']

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R✝ : Type u
K : Type u'
M✝ : Type v
V : Type v'
M₂✝ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type u_1
M₆ : Type u_2
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 : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
f : M →ₗ[R] M₂
C : Submodule R M
h : IsCompl C f.ker
y z : M
hy : y ∈ C
hz : z ∈ f.ker
⊢ ∃ a, (codRestrict f.range f ⋯ ∘ₗ C.subtype) a = ⟨f (y + z), ⋯⟩

Tactic:
use ⟨y, hy⟩

Goal state after:
case h
R✝ : Type u
K : Type u'
M✝ : Type v
V : Type v'
M₂✝ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type u_1
M₆ : Type u_2
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 : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
f : M →ₗ[R] M₂
C : Submodule R M
h : IsCompl C f.ker
y z : M
hy : y ∈ C
hz : z ∈ f.ker
⊢ (codRestrict f.range f ⋯ ∘ₗ C.subtype) ⟨y, hy⟩ = ⟨f (y + z), ⋯⟩
Module: Mathlib.Order.PartialSups

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
g : ι →o α
⊢ partialSups f ≤ g ↔ f ≤ ⇑g

Tactic:
refine ⟨(le_partialSups f).trans, fun h ↦ ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
g : ι →o α
h : f ≤ ⇑g
⊢ partialSups f ≤ g
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u_3
S : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
inst✝⁶ : RingHomSurjective σ
inst✝⁵ : AddCommMonoid G
inst✝⁴ : Module R G
inst✝³ : AddCommMonoid H
inst✝² : Module S H
inst✝¹ : AddCommMonoid I
inst✝ : Module S I
f : G →ₛₗ[σ] H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf₂ : Surjective (Prod.snd ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : H →ₗ[S] I
e₂ : I →ₗ[S] H
h : H
i : I
he₁ : ∀ (x : H × I), x ∈ f.range ↔ x.2 = e₁ x.1
he₂ : ∀ (x : I × H), x ∈ (↑(LinearEquiv.prodComm S H I) ∘ₛₗ f).range ↔ x.2 = e₂ x.1
⊢ i = e₁ h ↔ e₂ i = h

Tactic:
← he₁ (h, i),

Goal state after:
R : Type u_3
S : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
inst✝⁶ : RingHomSurjective σ
inst✝⁵ : AddCommMonoid G
inst✝⁴ : Module R G
inst✝³ : AddCommMonoid H
inst✝² : Module S H
inst✝¹ : AddCommMonoid I
inst✝ : Module S I
f : G →ₛₗ[σ] H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf₂ : Surjective (Prod.snd ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : H →ₗ[S] I
e₂ : I →ₗ[S] H
h : H
i : I
he₁ : ∀ (x : H × I), x ∈ f.range ↔ x.2 = e₁ x.1
he₂ : ∀ (x : I × H), x ∈ (↑(LinearEquiv.prodComm S H I) ∘ₛₗ f).range ↔ x.2 = e₂ x.1
⊢ (h, i) ∈ f.range ↔ e₂ i = h
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: S : Type u_4
H : Type u_6
I : Type u_7
inst✝⁴ : Semiring S
inst✝³ : AddCommMonoid H
inst✝² : Module S H
inst✝¹ : AddCommMonoid I
inst✝ : Module S I
G : Submodule S (H × I)
hG₁ : Bijective (Prod.fst ∘ ⇑G.subtype)
hG₂ : Bijective (Prod.snd ∘ ⇑G.subtype)
⊢ ∃ e, G = (↑e).graph

Tactic:
by
  simpa only [range_subtype] using LinearMap.exists_linearEquiv_eq_graph
    hG₁.surjective hG₂.surjective fun _ _ ↦ hG₁.injective.eq_iff.trans hG₂.injective.eq_iff.symm

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Monoid

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : ExistsAddOfLE M
a d : M
⊢ MapsTo (fun x ↦ x + d) (Ici a) (Ici (a + d))

Tactic:
by simp [MapsTo]

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Monoid

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : ExistsAddOfLE M
a d : M
⊢ MapsTo (fun x ↦ x + d) (Ioi a) (Ioi (a + d))

Tactic:
by simp [MapsTo]

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Monoid

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : ExistsAddOfLE M
a b d : M
⊢ MapsTo (fun x ↦ x + d) (Iic b) (Iic (b + d))

Tactic:
by simp [MapsTo]

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Monoid

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : ExistsAddOfLE M
a b d : M
⊢ MapsTo (fun x ↦ x + d) (Iio b) (Iio (b + d))

Tactic:
by simp [MapsTo]

Goal state after:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i0 ≤ i
⊢ 0 ≤ toZ i0 i

Tactic:
rw [toZ_of_ge hi]; exact Int.natCast_nonneg _

Goal state after:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case inr.inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 j i : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i < i0
hj : j < i0
⊢ -toZ i0 j ≤ -toZ i0 i

Tactic:
exact Int.neg_le_neg h_le

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

Goal state before:
pp: case neg
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
m n : ℕ
h : n ≤ m
⊢ ∏ k ∈ ∅, f k = ∏ k ∈ range 0, f (m + k)

Tactic:
range_zero,

Goal state after:
case neg
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
m n : ℕ
h : n ≤ m
⊢ ∏ k ∈ ∅, f k = ∏ k ∈ ∅, f (m + k)
Module: Mathlib.Order.Disjointed

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : OrderBot ι
f : ι → α
hf : Monotone f
m✝ n : ι
this : SuccOrder ι := LinearLocallyFiniteOrder.succOrder ι
m : ι
hm : n ≤ m
ih : (Ioc n m).sup (disjointed f) = f m \ f n
h'm : IsMax m
⊢ (Ioc n (succ m)).sup (disjointed f) = f (succ m) \ f n

pp: case neg
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : OrderBot ι
f : ι → α
hf : Monotone f
m✝ n : ι
this : SuccOrder ι := LinearLocallyFiniteOrder.succOrder ι
m : ι
hm : n ≤ m
ih : (Ioc n m).sup (disjointed f) = f m \ f n
h'm : ¬IsMax m
⊢ (Ioc n (succ m)).sup (disjointed f) = f (succ m) \ f n

Tactic:
· simpa [Order.succ_eq_iff_isMax.mpr h'm] using ih

Goal state after:
case neg
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : OrderBot ι
f : ι → α
hf : Monotone f
m✝ n : ι
this : SuccOrder ι := LinearLocallyFiniteOrder.succOrder ι
m : ι
hm : n ≤ m
ih : (Ioc n m).sup (disjointed f) = f m \ f n
h'm : ¬IsMax m
⊢ (Ioc n (succ m)).sup (disjointed f) = f (succ m) \ f n
Module: Mathlib.Data.Multiset.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ antidiagonal (n + 2) = (0, n + 2) ::ₘ (n + 2, 0) ::ₘ map (Prod.map Nat.succ Nat.succ) (antidiagonal n)

Tactic:
by
  rw [antidiagonal_succ, antidiagonal_succ', map_cons, map_map, Prod.map_apply]
  rfl

Goal state after:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : OrderBot ι
i j : ι
⊢ toZ ⊥ i ≤ ↑(toZ ⊥ j).toNat ↔ i ≤ j

Tactic:
← toZ_le_toZ (i0 := (⊥ : ι)),

Goal state after:
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : OrderBot ι
i j : ι
⊢ toZ ⊥ i ≤ ↑(toZ ⊥ j).toNat ↔ toZ ⊥ i ≤ toZ ⊥ j
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
n : ↥(Finset.range ((toZ ⊥ ⊤).toNat + 1))
⊢ (fun i ↦ ⟨(toZ ⊥ i).toNat, ⋯⟩) ((fun n ↦ succ^[↑n] ⊥) n) = n

Tactic:
ext1

Goal state after:
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
n : ↥(Finset.range ((toZ ⊥ ⊤).toNat + 1))
⊢ ↑((fun i ↦ ⟨(toZ ⊥ i).toNat, ⋯⟩) ((fun n ↦ succ^[↑n] ⊥) n)) = ↑n
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case pos
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
n : ↥(Finset.range ((toZ ⊥ ⊤).toNat + 1))
hn_max : succ^[↑n] ⊥ = ⊤
⊢ ↑n ≤ (toZ ⊥ (succ^[↑n] ⊥)).toNat

Tactic:
hn_max

Goal state after:
case pos
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
n : ↥(Finset.range ((toZ ⊥ ⊤).toNat + 1))
hn_max : succ^[↑n] ⊥ = ⊤
⊢ ↑n ≤ (toZ ⊥ ⊤).toNat
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
i j : ι
⊢ toZ ⊥ i ≤ ↑(toZ ⊥ j).toNat ↔ i ≤ j

Tactic:
← toZ_le_toZ (i0 := (⊥ : ι)),

Goal state after:
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
i j : ι
⊢ toZ ⊥ i ≤ ↑(toZ ⊥ j).toNat ↔ toZ ⊥ i ≤ toZ ⊥ j
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case zero
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
⊢ 1 = ∑ x ∈ range 0, t 0 x + t 0 0

Tactic:
range_zero,

Goal state after:
case zero
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
⊢ 1 = ∑ x ∈ ∅, t 0 x + t 0 0
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalRing R
inst✝ : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
hqp : IsIdempotentElem (q - p)
h : p * (q - p) + (q - p) * p = 0
⊢ Commute p q

Tactic:
simp_rw [IsIdempotentElem, mul_sub, sub_mul,
    hp.eq, hq.eq, ← sub_add_eq_sub_sub, sub_right_inj, add_sub] at hqp

Goal state after:
R : Type u_1
inst✝¹ : NonUnitalRing R
inst✝ : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
h : p * (q - p) + (q - p) * p = 0
hqp : p * q + q * p - p = p
⊢ Commute p q
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : CommRing α
x y z : α
⊢ span {x, y + z * x} = span {x, y}

Tactic:
by
  rw [mul_comm, span_pair_add_left_mul]

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

Goal state before:
pp: ι : Type u_1
R : ι → Type u_5
inst✝ : (i : ι) → Semiring (R i)
I J : (i : ι) → Ideal (R i)
le : pi I ≤ pi J
i : ι
r : R i
hr : r ∈ I i
⊢ r ∈ J i

Tactic:
classical simpa using le (single_mem_pi hr) i

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ ∏ i ∈ range (n + 2), f i (n + 1 - i) ^ (n + 1).choose i =
    (∏ i ∈ range (n + 1), f i (n + 1 - i) ^ n.choose i) * ∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ n.choose i

Tactic:
have A : (∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ (n.choose (i + 1))) * f 0 (n + 1) =
      ∏ i ∈ range (n + 1), f i (n + 1 - i) ^ (n.choose i) := by
    rw [prod_range_succ, prod_range_succ']; simp
  rw [prod_range_succ']
  simpa [choose_succ_succ, pow_add, prod_mul_distrib, A, mul_assoc] using mul_comm _ _

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

Goal state before:
pp: R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
hIm : I.IsMaximal
⊢ ∃ p, p ≠ ⊥ ∧ p.IsPrime

Tactic:
exact ⟨I, hI, hIm.isPrime⟩

Goal state after:
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
U : Set α
⊢ U ∈ ⋯.filter ↔ U ∈ l

Tactic:
simp [h.mem_iff, IsBasis.mem_filter_iff]

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: M : Type u_5
inst✝³ : AddCommMonoid M
X : Type u_6
Y : Type u_7
Z : Type u_8
inst✝² : Finite X
inst✝¹ : Finite Y
inst✝ : Finite Z
g : Y → Z
f : X → Y
s : X → M
x✝ : Z
⊢ map (g ∘ f) s x✝ = (map g ∘ map f) s x✝

Tactic:
simp [map, Finsupp.mapDomain_comp]

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Defs

Goal state before:
pp: α : Type u_3
inst✝ : Preorder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x ≤ y
⊢ atTop = generate (Ici '' s)

Tactic:
rw [atTop_eq_generate_Ici]

Goal state after:
α : Type u_3
inst✝ : Preorder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x ≤ y
⊢ generate (range Ici) = generate (Ici '' s)
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: case mp
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
t : Set α
⊢ (∃ t₁, (∃ i, p i ∧ s i ⊆ t₁) ∧ ∃ t₂, (∃ i, p' i ∧ s' i ⊆ t₂) ∧ t = t₁ ∩ t₂) →
    ∃ i, (p i.fst ∧ p' i.snd) ∧ s i.fst ∩ s' i.snd ⊆ t

Tactic:
rintro ⟨t, ⟨i, hi, ht⟩, t', ⟨i', hi', ht'⟩, rfl⟩

Goal state after:
case mp
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
t : Set α
i : ι
hi : p i
ht : s i ⊆ t
t' : Set α
i' : ι'
hi' : p' i'
ht' : s' i' ⊆ t'
⊢ ∃ i, (p i.fst ∧ p' i.snd) ∧ s i.fst ∩ s' i.snd ⊆ t ∩ t'
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
ι : Sort x
f : ι → Filter α
p : ι → Prop
l : Filter α
h : ∀ {s : Set α}, s ∈ l ↔ ∃ i, p i ∧ s ∈ f i
⊢ l = ⨅ i, ⨅ (_ : p i), f i

Tactic:
by
  rw [iInf_subtype']
  exact eq_iInf_of_mem_iff_exists_mem fun {_} => by simp only [Subtype.exists, h, exists_prop]

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
U : Set (Set α)
f : β → α
⊢ generate ((fun x ↦ f ⁻¹' x) '' U) ≤ comap f (generate U)

Tactic:
← map_le_iff_le_comap,

Goal state after:
α : Type u_1
β : Type u_2
U : Set (Set α)
f : β → α
⊢ map f (generate ((fun x ↦ f ⁻¹' x) '' U)) ≤ generate U
Module: Mathlib.Algebra.Module.TransferInstance

Goal state before:
pp: α : Type u_2
β : Type u_3
e : α ≃ β
R : Type u_4
inst✝³ : Zero R
inst✝² : Zero β
inst✝¹ : SMul R β
inst✝ : NoZeroSMulDivisors R β
this✝¹ : Zero α := e.zero
this✝ : SMul R α := Equiv.smul R e
⊢ NoZeroSMulDivisors R α

Tactic:
refine ⟨fun {r} m ↦ ?_⟩

Goal state after:
α : Type u_2
β : Type u_3
e : α ≃ β
R : Type u_4
inst✝³ : Zero R
inst✝² : Zero β
inst✝¹ : SMul R β
inst✝ : NoZeroSMulDivisors R β
this✝¹ : Zero α := e.zero
this✝ : SMul R α := Equiv.smul R e
r : R
m : α
⊢ r • m = 0 → r = 0 ∨ m = 0
Module: Mathlib.Algebra.Module.TransferInstance

Goal state before:
pp: α : Type u_2
β : Type u_3
e : α ≃ β
R : Type u_4
inst✝³ : Zero R
inst✝² : Zero β
inst✝¹ : SMul R β
inst✝ : NoZeroSMulDivisors R β
this✝¹ : Zero α := e.zero
this✝ : SMul R α := Equiv.smul R e
r : R
m : α
⊢ r • m = 0 → r = 0 ∨ m = 0

Tactic:
simpa [smul_def, zero_def, Equiv.eq_symm_apply] using eq_zero_or_eq_zero_of_smul_eq_zero

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

Goal state before:
pp: case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
⊢ lift.{v, u} (cof α) ≤ lift.{u, v} (cof β)

Tactic:
rw [le_lift_cof_iff]

Goal state after:
case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
⊢ ∀ (s : Set β), IsCofinal s → lift.{v, u} (cof α) ≤ lift.{u, v} #↑s
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
⊢ lift.{u, v} (cof β) ≤ lift.{v, u} (cof α)

Tactic:
rw [le_lift_cof_iff]

Goal state after:
case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
⊢ ∀ (s : Set α), IsCofinal s → lift.{u, v} (cof β) ≤ lift.{v, u} #↑s
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 : Type u_3
P : Type u_4
inst✝³ : Semiring S
inst✝² : AddCommMonoid P
inst✝¹ : Module S P
σ : R →+* S
inst✝ : RingHomSurjective σ
f : M →ₛₗ[σ] P
hf : Function.Injective ⇑f
N : Submodule R M
hfn : (map f N).FG
t : Finset P
ht : span S ↑t = map f N
⊢ ↑t ⊆ range ⇑f

Tactic:
rw [← LinearMap.coe_range, ← span_le, ht, ← map_top]

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_3
P : Type u_4
inst✝³ : Semiring S
inst✝² : AddCommMonoid P
inst✝¹ : Module S P
σ : R →+* S
inst✝ : RingHomSurjective σ
f : M →ₛₗ[σ] P
hf : Function.Injective ⇑f
N : Submodule R M
hfn : (map f N).FG
t : Finset P
ht : span S ↑t = map f N
⊢ map f N ≤ map f ⊤
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : β → α
g : α → β
h : GaloisConnection f g
⊢ lift.{u, v} (cof β) ≤ lift.{v, u} (cof α)

Tactic:
rw [le_lift_cof_iff]

Goal state after:
α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : β → α
g : α → β
h : GaloisConnection f g
⊢ ∀ (s : Set α), IsCofinal s → lift.{u, v} (cof β) ≤ lift.{v, u} #↑s
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁸ : Semiring α
inst✝⁷ : PartialOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
a₁ : α
b₁ b₂ : β
hb : b₁ ≤ b₂
a : α
ha₀ : 0 ≤ a
ha : a₁ ≤ a₁ + a
⊢ a₁ • b₂ + (a₁ + a) • b₁ ≤ a₁ • b₁ + (a₁ + a) • b₂

Tactic:
add_smul,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁸ : Semiring α
inst✝⁷ : PartialOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
a₁ : α
b₁ b₂ : β
hb : b₁ ≤ b₂
a : α
ha₀ : 0 ≤ a
ha : a₁ ≤ a₁ + a
⊢ a₁ • b₂ + (a₁ • b₁ + a • b₁) ≤ a₁ • b₁ + (a₁ + a) • b₂
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁸ : Semiring α
inst✝⁷ : PartialOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
a₁ : α
b₁ b₂ : β
hb : b₁ ≤ b₂
a : α
ha₀ : 0 ≤ a
ha : a₁ ≤ a₁ + a
⊢ a₁ • b₂ + (a₁ • b₁ + a • b₁) ≤ a₁ • b₁ + (a₁ + a) • b₂

Tactic:
add_smul,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁸ : Semiring α
inst✝⁷ : PartialOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
a₁ : α
b₁ b₂ : β
hb : b₁ ≤ b₂
a : α
ha₀ : 0 ≤ a
ha : a₁ ≤ a₁ + a
⊢ a₁ • b₂ + (a₁ • b₁ + a • b₁) ≤ a₁ • b₁ + (a₁ • b₂ + a • b₂)
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁸ : Semiring α
inst✝⁷ : PartialOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
a₁ a₂ : α
b₁ b₂ : β
ha : a₂ ≤ a₁
hb : b₂ ≤ b₁
⊢ a₁ • b₂ + a₂ • b₁ ≤ a₁ • b₁ + a₂ • b₂

Tactic:
simp_rw [add_comm (a₁ • _)]; exact smul_add_smul_le_smul_add_smul ha hb

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁸ : Semiring α
inst✝⁷ : PartialOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a₁ : α
b₁ b₂ : β
hb : b₁ < b₂
a : α
ha₀ : 0 < a
ha : a₁ < a₁ + a
⊢ a₁ • b₂ + (a₁ + a) • b₁ < a₁ • b₁ + (a₁ + a) • b₂

Tactic:
add_smul,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁸ : Semiring α
inst✝⁷ : PartialOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a₁ : α
b₁ b₂ : β
hb : b₁ < b₂
a : α
ha₀ : 0 < a
ha : a₁ < a₁ + a
⊢ a₁ • b₂ + (a₁ • b₁ + a • b₁) < a₁ • b₁ + (a₁ + a) • b₂
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁸ : Semiring α
inst✝⁷ : PartialOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a₁ : α
b₁ b₂ : β
hb : b₁ < b₂
a : α
ha₀ : 0 < a
ha : a₁ < a₁ + a
⊢ a₁ • b₂ + (a₁ • b₁ + a • b₁) < a₁ • b₁ + (a₁ + a) • b₂

Tactic:
add_smul,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁸ : Semiring α
inst✝⁷ : PartialOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a₁ : α
b₁ b₂ : β
hb : b₁ < b₂
a : α
ha₀ : 0 < a
ha : a₁ < a₁ + a
⊢ a₁ • b₂ + (a₁ • b₁ + a • b₁) < a₁ • b₁ + (a₁ • b₂ + a • b₂)