harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get?_alter [LawfulBEq α] (h : m.1.WF) {k k' : α} {f : Option (β k) → Option (β k)} :
    (m.alter k f).get? k' =
      if h : k == k' then
        cast (congrArg (Option ∘ β) (eq_of_beq h)) (f (m.get? k))
      else
        m.get? k'

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k k' : α
f : Option (β k) → Option (β k)
⊢ (m.alter k f).get? k' = if h : (k == k') = true then cast ⋯ (f (m.get? k)) else m.get? k'

Tactic:
simp_to_model [alter] using List.getValueCast?_alterKey

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Equiv.lean
theorem mem_support_finSuccEquiv {f : MvPolynomial (Fin (n + 1)) R} {x} :
    x ∈ (finSuccEquiv R n f).support ↔ x ∈ (fun m : Fin (n + 1) →₀ _ ↦ m 0) '' f.support

Proof state:
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
x : ℕ
⊢ x ∈ ((finSuccEquiv R n) f).support ↔ x ∈ (fun m => m 0) '' ↑f.support

Tactic:
simpa using congr(x ∈ $(support_finSuccEquiv f))

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem lift_sum {ι : Type u} (f : ι → Cardinal.{v}) :
    Cardinal.lift.{w} (Cardinal.sum f) = Cardinal.sum fun i => Cardinal.lift.{w} (f i) :=
  Equiv.cardinal_eq <|
    Equiv.ulift.trans <|
      Equiv.sigmaCongrRight fun a =>
    -- Porting note: Inserted universe hint .{_,_,v} below
        Nonempty.some <| by rw [← lift_mk_eq.{_,_,v}, mk_out, mk_out, lift_lift]

Proof state:
ι : Type u
f : ι → Cardinal.{v}
a : ι
⊢ Nonempty (Quotient.out (f a) ≃ Quotient.out ((fun i => lift.{w, v} (f i)) a))

Tactic:
rw [← lift_mk_eq.{_,_,v}, mk_out, mk_out, lift_lift]

Result:
no goals
-- Mathlib/Data/Option/Basic.lean
theorem none_orElse' (x : Option α) : none.orElse (fun _ ↦ x) = x

Proof state:
α : Type u_1
x : Option α
⊢ (none.orElse fun x_1 => x) = x

Tactic:
cases x <;> rfl

Result:
no goals
-- Mathlib/Data/Matrix/Block.lean
theorem vecMul_fromBlocks [Fintype n] [Fintype o] [NonUnitalNonAssocSemiring α] (A : Matrix n l α)
    (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) (x : n ⊕ o → α) :
    x ᵥ* fromBlocks A B C D =
      Sum.elim ((x ∘ Sum.inl) ᵥ* A + (x ∘ Sum.inr) ᵥ* C)
        ((x ∘ Sum.inl) ᵥ* B + (x ∘ Sum.inr) ᵥ* D)

Proof state:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝² : Fintype n
inst✝¹ : Fintype o
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
x : n ⊕ o → α
⊢ x ᵥ* fromBlocks A B C D = Sum.elim (x ∘ Sum.inl ᵥ* A + x ∘ Sum.inr ᵥ* C) (x ∘ Sum.inl ᵥ* B + x ∘ Sum.inr ᵥ* D)

Tactic:
ext i

Result:
case h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝² : Fintype n
inst✝¹ : Fintype o
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
x : n ⊕ o → α
i : l ⊕ m
⊢ (x ᵥ* fromBlocks A B C D) i = Sum.elim (x ∘ Sum.inl ᵥ* A + x ∘ Sum.inr ᵥ* C) (x ∘ Sum.inl ᵥ* B + x ∘ Sum.inr ᵥ* D) i

Proof state:
case h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝² : Fintype n
inst✝¹ : Fintype o
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
x : n ⊕ o → α
i : l ⊕ m
⊢ (x ᵥ* fromBlocks A B C D) i = Sum.elim (x ∘ Sum.inl ᵥ* A + x ∘ Sum.inr ᵥ* C) (x ∘ Sum.inl ᵥ* B + x ∘ Sum.inr ᵥ* D) i

Tactic:
cases i <;> simp [vecMul, dotProduct]

Result:
no goals
-- Mathlib/Combinatorics/Pigeonhole.lean
theorem exists_lt_sum_fiber_of_sum_fiber_nonpos_of_nsmul_lt_sum
    (ht : ∀ y ∉ t, ∑ x ∈ s with f x = y, w x ≤ 0)
    (hb : #t • b < ∑ x ∈ s, w x) : ∃ y ∈ t, b < ∑ x ∈ s with f x = y, w x :=
  exists_lt_of_sum_lt <|
    calc
      ∑ _y ∈ t, b < ∑ x ∈ s, w x

Proof state:
α : Type u
β : Type v
M : Type w
inst✝¹ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
w : α → M
b : M
inst✝ : LinearOrderedCancelAddCommMonoid M
ht : ∀ y ∉ t, ∑ x ∈ filter (fun x => f x = y) s, w x ≤ 0
hb : #t • b < ∑ x ∈ s, w x
⊢ ∑ _y ∈ t, b < ∑ x ∈ s, w x

Tactic:
simpa

Result:
no goals
-- Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean
theorem mem_primitiveRoots {ζ : R} (h0 : 0 < k) : ζ ∈ primitiveRoots k R ↔ IsPrimitiveRoot ζ k

Proof state:
R : Type u_4
k : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
h0 : 0 < k
⊢ ζ ∈ primitiveRoots k R ↔ IsPrimitiveRoot ζ k

Tactic:
rw [primitiveRoots, mem_filter, Multiset.mem_toFinset, mem_nthRoots h0, and_iff_right_iff_imp]

Result:
R : Type u_4
k : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
h0 : 0 < k
⊢ IsPrimitiveRoot ζ k → ζ ^ k = 1

Proof state:
R : Type u_4
k : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
h0 : 0 < k
⊢ ζ ∈ primitiveRoots k R ↔ IsPrimitiveRoot ζ k

Tactic:
classical
rw [primitiveRoots, mem_filter, Multiset.mem_toFinset, mem_nthRoots h0, and_iff_right_iff_imp]
exact IsPrimitiveRoot.pow_eq_one

Result:
no goals

Proof state:
R : Type u_4
k : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
h0 : 0 < k
⊢ IsPrimitiveRoot ζ k → ζ ^ k = 1

Tactic:
exact IsPrimitiveRoot.pow_eq_one

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean
theorem prod_range_zero (f : ℕ → β) : ∏ k ∈ range 0, f k = 1

Proof state:
β : Type u_4
inst✝ : CommMonoid β
f : ℕ → β
⊢ ∏ k ∈ range 0, f k = 1

Tactic:
rw [range_zero, prod_empty]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem msb_shiftLeftZeroExtend (x : BitVec w) (i : Nat) :
    (shiftLeftZeroExtend x i).msb = x.msb

Proof state:
w : Nat
x : BitVec w
i : Nat
⊢ (x.shiftLeftZeroExtend i).msb = x.msb

Tactic:
have : w + i - w ≤ i := by omega

Result:
w : Nat
x : BitVec w
i : Nat
this : w + i - w ≤ i
⊢ (x.shiftLeftZeroExtend i).msb = x.msb

Proof state:
w : Nat
x : BitVec w
i : Nat
⊢ w + i - w ≤ i

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
i : Nat
this : w + i - w ≤ i
⊢ (x.shiftLeftZeroExtend i).msb = x.msb

Tactic:
have : i + w - (w + i) = 0 := by omega

Result:
w : Nat
x : BitVec w
i : Nat
this✝ : w + i - w ≤ i
this : i + w - (w + i) = 0
⊢ (x.shiftLeftZeroExtend i).msb = x.msb

Proof state:
w : Nat
x : BitVec w
i : Nat
this✝ : w + i - w ≤ i
this : i + w - (w + i) = 0
⊢ (x.shiftLeftZeroExtend i).msb = x.msb

Tactic:
simp_all [shiftLeftZeroExtend_eq, BitVec.msb]

Result:
no goals

Proof state:
w : Nat
x : BitVec w
i : Nat
this : w + i - w ≤ i
⊢ i + w - (w + i) = 0

Tactic:
omega

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNorm'_measure_zero_of_neg {f : α → ε} (hq_neg : q < 0) :
    eLpNorm' f q (0 : Measure α) = ∞

Proof state:
α : Type u_1
ε : Type u_2
q : ℝ
inst✝¹ : ENorm ε
inst✝ : MeasurableSpace α
f : α → ε
hq_neg : q < 0
⊢ eLpNorm' f q 0 = ⊤

Tactic:
simp [eLpNorm', hq_neg]

Result:
no goals
-- Mathlib/Data/Option/Basic.lean
theorem pmap_map (g : γ → α) (x : Option γ) (H) :
    pmap f (x.map g) H = pmap (fun a h ↦ f (g a) h) x fun _ h ↦ H _ (mem_map_of_mem _ h)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
f : (a : α) → p a → β
g : γ → α
x : Option γ
H : ∀ (a : α), a ∈ Option.map g x → p a
⊢ pmap f (Option.map g x) H = pmap (fun a h => f (g a) h) x ⋯

Tactic:
cases x <;> simp only [map_none', map_some', pmap]

Result:
no goals
-- Mathlib/Tactic/NormNum/BigOperators.lean
lemma List.range_zero' {n : ℕ} (pn : NormNum.IsNat n 0) :
    List.range n = []

Proof state:
n : ℕ
pn : NormNum.IsNat n 0
⊢ List.range n = []

Tactic:
rw [pn.out, Nat.cast_zero, List.range_zero]

Result:
no goals
-- Mathlib/Data/Sign.lean
private lemma le_antisymm (a b : SignType) (_ : a ≤ b) (_ : b ≤ a) : a = b

Proof state:
a b : SignType
x✝¹ : a ≤ b
x✝ : b ≤ a
⊢ a = b

Tactic:
cases a <;> cases b <;> trivial

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get!_of_isEmpty [LawfulBEq α] (h : m.WF) {a : α} [Inhabited (β a)] :
    m.isEmpty = true → m.get! a = default

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
h : m.WF
a : α
inst✝ : Inhabited (β a)
⊢ m.isEmpty = true → m.get! a = default

Tactic:
simp_to_raw using Raw₀.get!_of_isEmpty ⟨m, _⟩

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean
theorem map_map {C : Type*} {M : Matrix m n A} {f : A → B} {g : B → C} :
    (M.map f).map g = M.map (g ∘ f)

Proof state:
case a
m : Type u_1
n : Type u_2
A : Type u_3
B : Type u_4
C : Type u_7
M : Matrix m n A
f : A → B
g : B → C
i✝ : m
j✝ : n
⊢ (M.map f).map g i✝ j✝ = M.map (g ∘ f) i✝ j✝

Tactic:
rfl

Result:
no goals

Proof state:
m : Type u_1
n : Type u_2
A : Type u_3
B : Type u_4
C : Type u_7
M : Matrix m n A
f : A → B
g : B → C
⊢ (M.map f).map g = M.map (g ∘ f)

Tactic:
ext

Result:
case a
m : Type u_1
n : Type u_2
A : Type u_3
B : Type u_4
C : Type u_7
M : Matrix m n A
f : A → B
g : B → C
i✝ : m
j✝ : n
⊢ (M.map f).map g i✝ j✝ = M.map (g ∘ f) i✝ j✝
-- Mathlib/Algebra/Polynomial/Mirror.lean
theorem natTrailingDegree_mul_mirror :
    (p * p.mirror).natTrailingDegree = 2 * p.natTrailingDegree

Proof state:
case pos
R : Type u_1
inst✝¹ : Semiring R
p : R[X]
inst✝ : NoZeroDivisors R
hp : p = 0
⊢ (p * p.mirror).natTrailingDegree = 2 * p.natTrailingDegree

Tactic:
rw [hp, zero_mul, natTrailingDegree_zero, mul_zero]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Semiring R
p : R[X]
inst✝ : NoZeroDivisors R
⊢ (p * p.mirror).natTrailingDegree = 2 * p.natTrailingDegree

Tactic:
by_cases hp : p = 0

Result:
case pos
R : Type u_1
inst✝¹ : Semiring R
p : R[X]
inst✝ : NoZeroDivisors R
hp : p = 0
⊢ (p * p.mirror).natTrailingDegree = 2 * p.natTrailingDegree

case neg
R : Type u_1
inst✝¹ : Semiring R
p : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
⊢ (p * p.mirror).natTrailingDegree = 2 * p.natTrailingDegree

Proof state:
case neg
R : Type u_1
inst✝¹ : Semiring R
p : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
⊢ (p * p.mirror).natTrailingDegree = 2 * p.natTrailingDegree

Tactic:
rw [natTrailingDegree_mul hp (mt mirror_eq_zero.mp hp), mirror_natTrailingDegree, two_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem nodup_range (n : Nat) : Nodup (range n)

Proof state:
n : Nat
⊢ (range n).Nodup

Tactic:
simp +decide only [range_eq_range', nodup_range']

Result:
no goals
-- Mathlib/Data/Multiset/Sort.lean
theorem mem_sort {s : Multiset α} {a : α} : a ∈ sort r s ↔ a ∈ s

Proof state:
α : Type u_1
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsTrans α r
inst✝¹ : IsAntisymm α r
inst✝ : IsTotal α r
s : Multiset α
a : α
⊢ a ∈ sort r s ↔ a ∈ s

Tactic:
rw [← mem_coe, sort_eq]

Result:
no goals
-- Mathlib/Data/Real/Irrational.lean
theorem sub_rat (h : Irrational x) : Irrational (x - q)

Proof state:
q : ℚ
x : ℝ
h : Irrational x
⊢ Irrational (x - ↑q)

Tactic:
simpa only [sub_eq_add_neg, cast_neg] using h.add_rat (-q)

Result:
no goals
-- Mathlib/CategoryTheory/Action/Limits.lean
/-- `F : C ⥤ Action V G` preserves the colimit of some `K : J ⥤ C` if
if it does after postcomposing with the forgetful functor `Action V G ⥤ V`. -/
lemma preservesColimit_of_preserves (F : C ⥤ Action V G) {J : Type w₁}
    [Category.{w₂} J] (K : J ⥤ C)
    (h : PreservesColimit K (F ⋙ Action.forget V G)) : PreservesColimit K F

Proof state:
V : Type (u + 1)
inst✝³ : LargeCategory V
G : Type u
inst✝² : Monoid G
C : Type t₁
inst✝¹ : Category.{t₂, t₁} C
F : C ⥤ Action V G
J : Type w₁
inst✝ : Category.{w₂, w₁} J
K : J ⥤ C
h : PreservesColimit K (F ⋙ forget V G)
F' : C ⥤ SingleObj G ⥤ V := F ⋙ (functorCategoryEquivalence V G).functor
⊢ PreservesColimit K F

Tactic:
have : PreservesColimit K F' := SingleObj.preservesColimit _ _ h

Result:
V : Type (u + 1)
inst✝³ : LargeCategory V
G : Type u
inst✝² : Monoid G
C : Type t₁
inst✝¹ : Category.{t₂, t₁} C
F : C ⥤ Action V G
J : Type w₁
inst✝ : Category.{w₂, w₁} J
K : J ⥤ C
h : PreservesColimit K (F ⋙ forget V G)
F' : C ⥤ SingleObj G ⥤ V := F ⋙ (functorCategoryEquivalence V G).functor
this : PreservesColimit K F'
⊢ PreservesColimit K F

Proof state:
V : Type (u + 1)
inst✝³ : LargeCategory V
G : Type u
inst✝² : Monoid G
C : Type t₁
inst✝¹ : Category.{t₂, t₁} C
F : C ⥤ Action V G
J : Type w₁
inst✝ : Category.{w₂, w₁} J
K : J ⥤ C
h : PreservesColimit K (F ⋙ forget V G)
⊢ PreservesColimit K F

Tactic:
let F' : C ⥤ SingleObj G ⥤ V := F ⋙ (Action.functorCategoryEquivalence V G).functor

Result:
V : Type (u + 1)
inst✝³ : LargeCategory V
G : Type u
inst✝² : Monoid G
C : Type t₁
inst✝¹ : Category.{t₂, t₁} C
F : C ⥤ Action V G
J : Type w₁
inst✝ : Category.{w₂, w₁} J
K : J ⥤ C
h : PreservesColimit K (F ⋙ forget V G)
F' : C ⥤ SingleObj G ⥤ V := F ⋙ (functorCategoryEquivalence V G).functor
⊢ PreservesColimit K F

Proof state:
V : Type (u + 1)
inst✝³ : LargeCategory V
G : Type u
inst✝² : Monoid G
C : Type t₁
inst✝¹ : Category.{t₂, t₁} C
F : C ⥤ Action V G
J : Type w₁
inst✝ : Category.{w₂, w₁} J
K : J ⥤ C
h : PreservesColimit K (F ⋙ forget V G)
F' : C ⥤ SingleObj G ⥤ V := F ⋙ (functorCategoryEquivalence V G).functor
this : PreservesColimit K F'
⊢ PreservesColimit K F

Tactic:
apply preservesColimit_of_reflects_of_preserves F (Action.functorCategoryEquivalence V G).functor

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Basic.lean
@[simp]
lemma prod_X_pow_eq_monomial : ∏ x ∈ s.support, X x ^ s x = monomial s (1 : R)

Proof state:
R : Type u
σ : Type u_1
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ ∏ x ∈ s.support, X x ^ s x = (monomial s) 1

Tactic:
simp only [monomial_eq, map_one, one_mul, Finsupp.prod]

Result:
no goals
-- Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean
theorem ιMulti_succ_curryLeft {n : ℕ} (m : M) :
    (ιMulti R n.succ).curryLeft m = (LinearMap.mulLeft R (ι R m)).compAlternatingMap (ιMulti R n) :=
  AlternatingMap.ext fun v =>
    (ιMulti_succ_apply _).trans <| by
      simp_rw [Matrix.tail_cons]
      rfl

Proof state:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
m : M
v : Fin n → M
⊢ (ι R) (Matrix.vecCons m v 0) * (ιMulti R n) (Matrix.vecTail (Matrix.vecCons m v)) =
    ((LinearMap.mulLeft R ((ι R) m)).compAlternatingMap (ιMulti R n)) v

Tactic:
simp_rw [Matrix.tail_cons]

Result:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
m : M
v : Fin n → M
⊢ (ι R) (Matrix.vecCons m v 0) * (ιMulti R n) v = ((LinearMap.mulLeft R ((ι R) m)).compAlternatingMap (ιMulti R n)) v

Proof state:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
m : M
v : Fin n → M
⊢ (ι R) (Matrix.vecCons m v 0) * (ιMulti R n) v = ((LinearMap.mulLeft R ((ι R) m)).compAlternatingMap (ιMulti R n)) v

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/ENNReal/Basic.lean
theorem coe_mem_upperBounds {s : Set ℝ≥0} :
    ↑r ∈ upperBounds (ofNNReal '' s) ↔ r ∈ upperBounds s

Proof state:
r : ℝ≥0
s : Set ℝ≥0
⊢ ↑r ∈ upperBounds (ofNNReal '' s) ↔ r ∈ upperBounds s

Tactic:
simp +contextual [upperBounds, forall_mem_image, -mem_image, *]

Result:
no goals
-- Mathlib/Data/Matroid/Sum.lean
@[simp] lemma sum_indep_iff (M : Matroid α) (N : Matroid β) {I : Set (α ⊕ β)} :
    (M.sum N).Indep I ↔ M.Indep (.inl ⁻¹' I) ∧ N.Indep (.inr ⁻¹' I)

Proof state:
α : Type u
β : Type v
M : Matroid α
N : Matroid β
I : Set (α ⊕ β)
⊢ M.Indep
        ((fun a => Equiv.ulift a) ''
          (Sigma.mk false ⁻¹'
            ((fun a => (Equiv.sumEquivSigmaBool (ULift.{v, u} α) (ULift.{u, v} β)) a) ''
              ((fun a => Sum.map (⇑Equiv.ulift.symm) (⇑Equiv.ulift.symm) a) '' I)))) ∧
      N.Indep
        ((fun a => Equiv.ulift a) ''
          (Sigma.mk true ⁻¹'
            ((fun a => (Equiv.sumEquivSigmaBool (ULift.{v, u} α) (ULift.{u, v} β)) a) ''
              ((fun a => Sum.map (⇑Equiv.ulift.symm) (⇑Equiv.ulift.symm) a) '' I)))) ↔
    M.Indep (Sum.inl ⁻¹' I) ∧ N.Indep (Sum.inr ⁻¹' I)

Tactic:
convert Iff.rfl <;>
  simp [Set.ext_iff, Equiv.ulift, Equiv.sumEquivSigmaBool]

Result:
no goals

Proof state:
α : Type u
β : Type v
M : Matroid α
N : Matroid β
I : Set (α ⊕ β)
⊢ (M.sum N).Indep I ↔ M.Indep (Sum.inl ⁻¹' I) ∧ N.Indep (Sum.inr ⁻¹' I)

Tactic:
simp only [Matroid.sum, mapEquiv_indep_iff, Equiv.sumCongr_symm, Equiv.sumCongr_apply,
  Equiv.symm_symm, sigma_indep_iff, Bool.forall_bool, Equiv.ulift_apply]

Result:
α : Type u
β : Type v
M : Matroid α
N : Matroid β
I : Set (α ⊕ β)
⊢ M.Indep
        ((fun a => Equiv.ulift a) ''
          (Sigma.mk false ⁻¹'
            ((fun a => (Equiv.sumEquivSigmaBool (ULift.{v, u} α) (ULift.{u, v} β)) a) ''
              ((fun a => Sum.map (⇑Equiv.ulift.symm) (⇑Equiv.ulift.symm) a) '' I)))) ∧
      N.Indep
        ((fun a => Equiv.ulift a) ''
          (Sigma.mk true ⁻¹'
            ((fun a => (Equiv.sumEquivSigmaBool (ULift.{v, u} α) (ULift.{u, v} β)) a) ''
              ((fun a => Sum.map (⇑Equiv.ulift.symm) (⇑Equiv.ulift.symm) a) '' I)))) ↔
    M.Indep (Sum.inl ⁻¹' I) ∧ N.Indep (Sum.inr ⁻¹' I)
-- Mathlib/Topology/Sets/Closeds.lean
theorem coe_iInf {ι} (s : ι → Closeds α) : ((⨅ i, s i : Closeds α) : Set α) = ⋂ i, s i

Proof state:
case h
α : Type u_2
inst✝ : TopologicalSpace α
ι : Sort u_4
s : ι → Closeds α
x✝ : α
⊢ x✝ ∈ ↑(⨅ i, s i) ↔ x✝ ∈ ⋂ i, ↑(s i)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_2
inst✝ : TopologicalSpace α
ι : Sort u_4
s : ι → Closeds α
⊢ ↑(⨅ i, s i) = ⋂ i, ↑(s i)

Tactic:
ext

Result:
case h
α : Type u_2
inst✝ : TopologicalSpace α
ι : Sort u_4
s : ι → Closeds α
x✝ : α
⊢ x✝ ∈ ↑(⨅ i, s i) ↔ x✝ ∈ ⋂ i, ↑(s i)
-- Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean
theorem natAbs_norm_mod_lt (x : ℤ[i]) {y : ℤ[i]} (hy : y ≠ 0) :
    (x % y).norm.natAbs < y.norm.natAbs :=
  Int.ofNat_lt.1 (by simp [-Int.ofNat_lt, norm_mod_lt x hy])

Proof state:
x y : ℤ[i]
hy : y ≠ 0
⊢ ↑(norm (x % y)).natAbs < ↑(norm y).natAbs

Tactic:
simp [-Int.ofNat_lt, norm_mod_lt x hy]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Ico_union_Ico' {a b c d : α} (hcb : c ≤ b) (had : a ≤ d) :
    Ico a b ∪ Ico c d = Ico (min a c) (max b d)

Proof state:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
hcb : c ≤ b
had : a ≤ d
⊢ Ico a b ∪ Ico c d = Ico (a ⊓ c) (b ⊔ d)

Tactic:
rw [← coe_inj, coe_union, coe_Ico, coe_Ico, coe_Ico, Set.Ico_union_Ico' hcb had]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/PiTensorProduct/InjectiveSeminorm.lean
theorem mapL_id : mapL (fun i ↦ ContinuousLinearMap.id 𝕜 (E i)) = ContinuousLinearMap.id _ _

Proof state:
ι : Type uι
inst✝³ : Fintype ι
𝕜 : Type u𝕜
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
⊢ (mapL fun i => ContinuousLinearMap.id 𝕜 (E i)) = ContinuousLinearMap.id 𝕜 (⨂[𝕜] (i : ι), E i)

Tactic:
apply ContinuousLinearMap.coe_injective

Result:
case a
ι : Type uι
inst✝³ : Fintype ι
𝕜 : Type u𝕜
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
⊢ ↑(mapL fun i => ContinuousLinearMap.id 𝕜 (E i)) = ↑(ContinuousLinearMap.id 𝕜 (⨂[𝕜] (i : ι), E i))

Proof state:
case a.H.H
ι : Type uι
inst✝³ : Fintype ι
𝕜 : Type u𝕜
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
x✝ : (i : ι) → E i
⊢ ((↑(mapL fun i => ContinuousLinearMap.id 𝕜 (E i))).compMultilinearMap (tprod 𝕜)) x✝ =
    ((↑(ContinuousLinearMap.id 𝕜 (⨂[𝕜] (i : ι), E i))).compMultilinearMap (tprod 𝕜)) x✝

Tactic:
simp only [mapL_coe, ContinuousLinearMap.coe_id, map_id, LinearMap.compMultilinearMap_apply,
  LinearMap.id_coe, id_eq]

Result:
no goals

Proof state:
case a
ι : Type uι
inst✝³ : Fintype ι
𝕜 : Type u𝕜
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
⊢ ↑(mapL fun i => ContinuousLinearMap.id 𝕜 (E i)) = ↑(ContinuousLinearMap.id 𝕜 (⨂[𝕜] (i : ι), E i))

Tactic:
ext

Result:
case a.H.H
ι : Type uι
inst✝³ : Fintype ι
𝕜 : Type u𝕜
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
x✝ : (i : ι) → E i
⊢ ((↑(mapL fun i => ContinuousLinearMap.id 𝕜 (E i))).compMultilinearMap (tprod 𝕜)) x✝ =
    ((↑(ContinuousLinearMap.id 𝕜 (⨂[𝕜] (i : ι), E i))).compMultilinearMap (tprod 𝕜)) x✝
-- Mathlib/Data/ENNReal/Real.lean
theorem toNNReal_pos_iff : 0 < a.toNNReal ↔ 0 < a ∧ a < ∞

Proof state:
a : ℝ≥0∞
⊢ 0 < a.toNNReal ↔ 0 < a ∧ a < ⊤

Tactic:
induction a <;> simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Degree.lean
lemma natDegree_map_lt (hp : f p.leadingCoeff = 0) (hp₀ : map f p ≠ 0) :
    (p.map f).natDegree < p.natDegree :=
  natDegree_lt_natDegree hp₀ <| degree_map_lt hp <| by rintro rfl; simp at hp₀

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
hp : f p.leadingCoeff = 0
hp₀ : map f p ≠ 0
⊢ p ≠ 0

Tactic:
rintro rfl

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hp : f (leadingCoeff 0) = 0
hp₀ : map f 0 ≠ 0
⊢ False

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hp : f (leadingCoeff 0) = 0
hp₀ : map f 0 ≠ 0
⊢ False

Tactic:
simp at hp₀

Result:
no goals
-- Mathlib/Analysis/Normed/Module/FiniteDimension.lean
theorem lipschitzExtensionConstant_pos (E' : Type*) [NormedAddCommGroup E'] [NormedSpace ℝ E']
    [FiniteDimensional ℝ E'] : 0 < lipschitzExtensionConstant E'

Proof state:
E' : Type u_1
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : FiniteDimensional ℝ E'
⊢ 0 < lipschitzExtensionConstant E'

Tactic:
rw [lipschitzExtensionConstant]

Result:
E' : Type u_1
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : FiniteDimensional ℝ E'
⊢ 0 <
    let A := (Basis.ofVectorSpace ℝ E').equivFun.toContinuousLinearEquiv;
    ‖↑A.symm‖₊ * ‖↑A‖₊ ⊔ 1

Proof state:
E' : Type u_1
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : FiniteDimensional ℝ E'
⊢ 0 <
    let A := (Basis.ofVectorSpace ℝ E').equivFun.toContinuousLinearEquiv;
    ‖↑A.symm‖₊ * ‖↑A‖₊ ⊔ 1

Tactic:
exact zero_lt_one.trans_le (le_max_right _ _)

Result:
no goals
-- Mathlib/RingTheory/Flat/Basic.lean
theorem linearIndependent_one_tmul {S} [Semiring S] [Algebra R S] [Flat R S] {ι} {v : ι → M}
    (hv : LinearIndependent R v) : LinearIndependent S ((1 : S) ⊗ₜ[R] v ·)

Proof state:
R : Type u
M : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Algebra R S
inst✝ : Flat R S
ι : Type u_5
v : ι → M
hv : LinearIndependent R v
⊢ LinearIndependent S fun x => 1 ⊗ₜ[R] v x

Tactic:
rw [LinearIndependent, ← LinearMap.coe_restrictScalars R,
Finsupp.linearCombination_one_tmul]

Result:
R : Type u
M : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Algebra R S
inst✝ : Flat R S
ι : Type u_5
v : ι → M
hv : LinearIndependent R v
⊢ Function.Injective ⇑(lTensor S (Finsupp.linearCombination R v) ∘ₗ ↑(finsuppScalarRight R S ι).symm)

Proof state:
R : Type u
M : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Algebra R S
inst✝ : Flat R S
ι : Type u_5
v : ι → M
hv : LinearIndependent R v
⊢ LinearIndependent S fun x => 1 ⊗ₜ[R] v x

Tactic:
classical rw [LinearIndependent, ← LinearMap.coe_restrictScalars R,
  Finsupp.linearCombination_one_tmul]

Result:
R : Type u
M : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Algebra R S
inst✝ : Flat R S
ι : Type u_5
v : ι → M
hv : LinearIndependent R v
⊢ Function.Injective ⇑(lTensor S (Finsupp.linearCombination R v) ∘ₗ ↑(finsuppScalarRight R S ι).symm)

Proof state:
R : Type u
M : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Algebra R S
inst✝ : Flat R S
ι : Type u_5
v : ι → M
hv : LinearIndependent R v
⊢ Function.Injective ⇑(lTensor S (Finsupp.linearCombination R v) ∘ₗ ↑(finsuppScalarRight R S ι).symm)

Tactic:
simpa using lTensor_preserves_injective_linearMap _ hv

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem bsup_one (f : ∀ a < (1 : Ordinal), Ordinal) : bsup 1 f = f 0 zero_lt_one

Proof state:
f : (a : Ordinal.{u_4}) → a < 1 → Ordinal.{max u_4 u_5}
⊢ bsup 1 f = f 0 ⋯

Tactic:
simp_rw [← sup_eq_bsup, sup_unique, familyOfBFamily, familyOfBFamily', typein_one_toType]

Result:
no goals